公开(公告)号：US09158874B1

公开(公告)日：2015-10-13

申请号：US14073787

申请日：2013-11-06

Applicant: Jasper Design Automation, Inc.

Inventor： Rajeev K. Ranjan ,  Ross M. Weber ,  Habeeb A. Farah ,  Ziyad E. Hanna

IPC: G06F17/50

CPC classification number: G06F17/504 ,  G06F17/50 ,  G06F17/5022 ,  G06F17/5081

Abstract: A computer-implemented method and non-transitory computer readable medium for circuit design verification. A property defined for a circuit design is received, the property having a cone of influence in the circuit design corresponding to a portion of the circuit design capable of affecting the property. Bounded reachability analysis is performed for the circuit design against a set of cover items. The set of cover items are classified into classified cover items based on results of the reachability analysis. Coverage information is generated indicating an amount of formal verification coverage provided by the property. The coverage information is generated based on a first set of the classified cover items that correspond to the cone of influence of the property and that are reached within a particular bound during the reachability analysis.

Abstract translation: 一种用于电路设计验证的计算机实现的方法和非暂时性计算机可读介质。 接收为电路设计定义的属性，该属性在电路设计中具有与影响该性能的电路设计的一部分相对应的影响锥。 对一套封面项目进行电路设计的有界可达性分析。 根据可达性分析的结果，将一套封面项目分类为分类覆盖项目。 生成指示由属性提供的正式验证覆盖量的覆盖信息。 覆盖信息是基于对应于属性的影响锥度并且在可达性分析期间在特定边界内达到的分类覆盖项目的第一组生成的。

公开(公告)号：US08826201B1

公开(公告)日：2014-09-02

申请号：US13826801

申请日：2013-03-14

Applicant: Jasper Design Automation, Inc.

Inventor： Ziyad E. Hanna ,  Per Anders M. Franzén ,  Ross M. Weber ,  Habeeb A. Farah ,  Rajeev K. Ranjan

IPC: G06F9/455 ,  G06F17/50

CPC classification number: G06F17/5045 ,  G06F17/504

Abstract: A computer-implemented method and non-transitory computer readable medium for circuit design verification. Formal verification is performed on a circuit design to prove a correctness of a property of the circuit design. The circuit design has a cone of influence representing a portion of the circuit design capable of affecting signals of the property. A proof core of the circuit design is identified, the proof core being a portion of the cone of influence that is sufficient to prove the correctness of the property. A coverage metric is generated that is indicative of a level of formal verification coverage provided by the property based on the proof core of the circuit design.

Abstract translation: 一种用于电路设计验证的计算机实现的方法和非暂时性计算机可读介质。 对电路设计进行正式验证，以证明电路设计的属性的正确性。 电路设计具有代表电路设计能够影响该特性的信号的一部分的影响锥。 识别电路设计的核心，防爆核心是足以证明属性正确性的影响力的一部分。 产生一个覆盖度量，其指示由基于电路设计的验证核心的属性提供的形式验证覆盖水平。