Formal verification coverage metrics for circuit design properties

摘要

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.

主权项

1. A computer-implemented method for circuit design verification, comprising:
performing formal verification on a circuit design to prove correctness of at least one property of the circuit design, the circuit design having a cone of influence representing a portion of the circuit design; identifying multiple proof cores of the circuit design, at least a first proof core of the multiple proof cores being a portion of the cone of influence and being sufficient to prove unsatisfiability of a representation of the at least one property; and generating, by a computing system, a coverage metric that is indicative of a level of formal verification coverage provided by the at least one property at least by determining an intersection between a coverage model and at least a part of the multiple proof cores of the circuit design.