Measure of analysis performed in property checking
View Patent ↗The amount of analysis performed in determining the validity of a property of a digital circuit is measured concurrent with performance of the analysis, and provided as an output when a true/false answer cannot be provided e.g. when stopped due to resource constraints. In some embodiments, a measure of value N indicates that a given property that is being checked will not be violated within a distance N from an initial state from which the analysis started. Therefore, in such embodiments, a measure of value N indicates that the analysis has implicitly or explicitly covered every possible excursion of length N from the initial state, and formally proved that no counter-example is possible within this length N.
1. A method for determining a performance rating of a formal verification tool, the method comprising:
by a computer, determining a proof radius indicative of an amount of analysis performed for a property of a circuit without finding a counter-example for the property when using the formal verification tool to formally verify the property until a predetermined limit is met;
by the computer, determining a performance rating for the formal verification tool, wherein the performance rating is based at least in part on the proof radius; and
displaying the performance rating;
wherein the predetermined limit is based at least in part on a predetermined budget of processing time that elapses during the formally verifying or on a reaching a proof radius limit during the formally verifying.
2. The method of claim 1 , wherein the predetermined limit is at least partially specified by a user.
3. One or more non-transitory machine-readable storage media storing machine-readable instructions that when executed by a computer cause the computer to perform a method for determining a performance rating of a formal verification tool, the method comprising:
determining a proof radius indicative of an amount of analysis performed for a property of a circuit without finding a counter-example for the property to formally verify the property with the formal verification tool until a predetermined limit is met;
determining a performance rating for the formal verification tool, wherein the performance rating is based at least in part on the proof radius; and
displaying the performance rating;
wherein the predetermined limit is based at least in part on a predetermined budget of processing time that elapses during the formally verifying or on a reaching a proof radius limit during the formally verifying.
4. The non-transitory machine-readable storage media of claim 3 , wherein the determined proof radius is a minimum proof radius, an average proof radius, or a maximum proof radius achieved during analysis of the circuit from one or more seed states.
5. A system comprising a computer having one or more hardware processors and the non-transitory machine-readable storage media of claim 3 .