Patent ID: 8032848

Claim:
A method to verify a property for a circuit design, the method comprising: determining a first counter-example for the property using a first abstract model of the circuit design, wherein the property is associated with a set of state variables, and wherein the first abstract model includes all state variables whose distance from at least one state variable in the set of state variables is less than or equal to a lower-bound-distance; and verifying, by computer, the property based on an abstraction-refinement technique, wherein said verifying includes: determining an upper-bound-distance for a second abstract model of the circuit design, wherein the upper-bound-distance is equal to the largest distance in a set of distances between state variables in the set of state variables and state variables in the second abstract model; and in response to determining that the lower-bound-distance is greater than or equal to the upper-bound-distance, determining a second counter example for the property without performing a reachability analysis on the second abstract model.