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 implemented in a programmed computer, the method comprising a plurality of acts, said plurality of acts comprising:
formally verifying a property of a digital circuit for at least one iteration of a formal verification method using a description of said digital circuit, said description being expressed using a hardware description language;
increasing a measure of analysis if said property remains true at the end of said iteration;
iteratively repeating the act of formally verifying and the act of increasing until use of a resource reaches a first predetermined limit or said measure reaches a second predetermined limit determining if the use of the resource reaches said first predetermined limit and if said measure reaches said second predetermined limit;
displaying a report based on said measure; and
setting said measure to an initial value prior to formal verification.
2. The method of claim 1 , wherein said hardware description language is Verilog.
3. The method of claim 1 , wherein said hardware description language is VHDL.
4. The method of claim 1 , wherein said property is at least partially specified by the user.
5. The method of claim 1 , wherein said description includes a plurality of properties.
6. The method of claim 5 , further comprising using said measure to identify a property for further analysis.
7. The method of claim 1 , wherein said description includes at least one checker.
8. The method of claim 7 , wherein said checker is at least partially specified by the user.
9. The method of claim 1 , wherein said description includes a plurality of checkers.
10. The method of claim 1 , wherein said description includes at least one constraint.
11. The method of claim 10 , wherein said constraint is at least partially specified by the user.
12. The method of claim 1 , wherein said description includes a plurality of constraints.
13. The method of claim 1 , wherein said digital circuit contains at least two clock signals operating at different frequencies.
14. The method of claim 1 , wherein formally verifying comprises searching for an input sequence that will cause a property to be violated.
15. The method of claim 1 , wherein formally verifying comprises performing a breadth-first search.
16. The method of claim 1 , further comprising using said measure as a guide for further testing.
17. The method of claim 1 , further comprising using said measure as a guide for terminating testing.
18. The method of claim 1 , wherein said first predetermined limit is at least partially specified by the user.
19. The method of claim 1 , wherein said second predetermined limit is at least partially specified by the user.
20. The method of claim 1 , wherein said initial value is zero.
21. The method of claim 1 , wherein said initial value is one.
22. The method of claim 1 , wherein iteratively repeating comprising iteratively repeating the act of formally verifying, the act of increasing, and the act of determining until use of said resource reaches said first predetermined limit or said measure reaches said second predetermined limit.
23. The method of claim 1 , wherein said first predetermined limit is a measure of a depth of search without finding a counter-example.
24. The method of claim 1 , wherein said second predetermined limit comprises a measure of usage of computing resources.
25. An apparatus for formally verifying a property of a digital circuit, the apparatus comprising:
a processor;
a machine-readable medium including instructions executable by the processor for formally verifying a property of a digital circuit for at least one iteration of a formal verification method using a description of said digital circuit, said description being expressed using a hardware description language;
increasing a measure of analysis if said property remains true at the end of said iteration;
iteratively repeating the act of formally verifying and the act of increasing until use of a resource reaches a first predetermined limit or said measure reaches a second predetermined limit determining if the use of the resource reaches said first predetermined limit and if said measure reaches said second predetermined limit,
displaying a report based on said measure; and
setting said measure to an initial value prior to formal verification.
26. A machine-readable medium including instructions executable by a processor for formally verifying a property of a digital circuit, the machine-readable medium comprising:
one or more instructions for formally verifying a property of a digital circuit for at least one iteration of a formal verification method using a description of said digital circuit, said description being expressed using a hardware description language;
one or more instructions for increasing a measure of analysis if said property remains true at the end of said iteration;
one or more instructions for iteratively repeating the act of formally verifying and the act of increasing until use of a resource reaches a first predetermined limit or said measure reaches a second predetermined limit one or more instructions for determining if the use of the resource reaches said first predetermined limit and if said measure reaches said second predetermined limit;
one or more instructions for displaying a report based on said measure; and
one or more instructions for setting said measure to an initial value prior to formal verification.