Measure of analysis performed in property checking

A machine-readable storage medium storing instructions executable by a processor for performing a method, the method comprising:

• formally verifying a property of a digital circuit by applying an analysis tool to analyze at least one cycle of operation of the digital circuit;
• iteratively repeating the formally verifying and increasing a measure of analysis unless a counterexample is discovered;
• determining a first value for a use of a resource and a second value for the measure of analysis;
• stopping the iteratively repeating when the first value for the use of the resource reaches a first predetermined limit;
• and
• outputting a report based on the second value for the measure of analysis.

A method, comprising:

• receiving data selecting a value of an effort variable;
• using a computer, formally verifying a property of a digital circuit by applying an analysis tool to analyze at least one cycle of operation of the digital circuit;
• increasing a measure of analysis if the property remains true at the end of the at least one cycle of operation;
• iteratively repeating the formally verifying and the increasing the measure of analysis unless a predetermined condition is met, the predetermined condition depending at least in part on the value of the effort variable;
• stopping the iteratively repeating upon meeting the predetermined condition;
• and
• outputting data based on the measure of analysis.