Patent ID: 7469392
Filing Date: 2008-12-23
Classification: G06F

Abstract:
1. A method for refining an abstract model, the method comprising: receiving an abstract model which is a subset of a logic design, wherein the abstract model is represented using a set of variables and a set of Boolean functions; receiving a safety property for the logic design which is desired to be proven; receiving a set of counter-examples, wherein a counter-example is a sequence of states that violates the safety property, wherein a state is an assignment of values to the variables, wherein the variable values are determined using the set of Boolean functions and the variable values in the previous state; determining a set of cooperative variables using the set of counter-examples, wherein a cooperative variable is a variable that helps invalidate a counter-example; and refining the abstract model using the set of cooperative variables; wherein the safety property specifies an initial state and a fail variable; wherein a counter-example is a sequence of states which begins with the initial state, and ends with a state in which the fail variable is true; wherein the safety property is proven for the logic design if and only if there does not exist a counter-example for the safety property; and wherein proving the safety property for the abstract model is equivalent to proving the safety property for the logic design.