Formal verification coverage metrics for circuit design properties

A non-transitory computer readable medium storing thereupon processor executable instructions for circuit design verification, the processor executable instructions comprising instructions which, when executed by at least one micro-processor of a computing system, causes the at least one micro-processor to perform a series of acts for circuit:

• design verification, the series of acts 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.

A system for circuit design verification, comprising:

• one or more mechanisms, at least one of which comprises at least one microprocessor including one or more processor cores executing one or more threads in a computing system;
• a non-transitory computer accessible storage medium storing thereupon program code that includes a sequence of instructions that, when executed by the at least one micro-processor or processor core of a computing system, causes the at least one micro-processor or processor core at least to:
• 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 the at least one microprocessor, 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.