Efficient approaches for bounded model checking

1. A method for bounded model checking of arbitrary Linear Temporal Logic (LTL) properties in a verification engine for verification circuits which is capable of bounded model checking the method comprising:

in a verification engine,

translating by a computer configured by said verification engine LTL properties expressed with one or more LTL operators F(p), G(p), U(p,q) and X(p) into property checking schemas for performing Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator, X represents a next-time operator, p represents either an atomic proposition or a Boolean combination of LTL operators, and q represents either an atomic proposition or a Boolean combination of LTL operators,

checking by the said computer the said properties by invoking repeatedly one or more property checking schemas for F(p), G(p), U(p,q) and X(p) operators, and using the results of the checking to indicate if a circuit performs according to the said properties, wherein

a subset of the property checking schemas is customized to perform a partitioning of a k th instance of a corresponding bounded model checking problem into multiple smaller Boolean satisfiability sub-problems, wherein

the partitioning is performed across said LTL operators, and for each said operator both across time frames and within time frames, wherein

when a choice exists about which said operator to check next, the choice is made according to priority determined by degree of difficulty of search estimated to be increasing in the following order: atomic propositions, X operator, F operator, U operator, G operator.

2. The method of claim 1 wherein an incremental formulation of a Boolean satisfiability algorithm is used to solve the said Boolean sub-problems.

3. The method of claim 1 wherein circuit simplification based on constant propagation is further used to simplify the said Boolean satisfiability sub-problems.

4. The method of claim 1 wherein circuit simplification based on detection of structural isomorphism is further used to simplify the Boolean satisfiability sub-problems.

5. The method of claim 1 wherein the said Boolean satisfiability sub-problems are solved by using a hybrid Boolean Satisfiability (SAT) solver that combines circuit-based and Conjunctive Normal Form—based (CNF-based) satisfiability checking techniques.

6. The method of claim 1 wherein the property checking schema for the said LTL operator F(p) for a given time frame bound comprises:

a) starting search from a given start state at time frame i, with a given constraint database, wherein i=0 corresponds to an initial state of the circuit;

b) checking for satisfiability of p in the i th state of a path,

c) if satisfiable, terminating the search with success;

d) if unsatisfiable, learning that p is always false in the i th state and adding this learnt knowledge to a constraint database;

e) continuing the search by increasing i until the said time frame bound is reached, and repeating steps b-d; and

f) terminating the search inconclusively if the said time frame bound is reached.

7. The method of claim 6 further comprising checking for completeness of the solution between steps d and e, to determine failure wherein, failure characterizes that the said success in step c is not achievable for any time frame i.

8. The method of claim 7 wherein the checking for completeness further comprises:

(i) adding constraints to ensure that same states are not revisited in the said path, and checking satisfiability of the constraint database;

(ii) if unsatisfiable, terminating the search with the said failure,

(iii) otherwise, continuing search; and

(iv) repeating steps (i)-(iii) until all previous states have been examined.

9. The method of claim 6 , wherein a subset of satisfiability checks is combined into a single satisfiability check.

10. The method in claim 1 wherein the property checking schema for the said LTL operator G(p) for a given time frame bound comprises:

a) starting search from a given start state at time frame i with a given constraint database, wherein i=0 corresponds to an initial state of the circuit,

b) adding a constraint to the database to ensure that p is satisfied in the i th state of a path, and checking for satisfiability,

c) if unsatisfiable, terminating the search with failure,

d) if satisfiable, checking for each j th state from the start state to i th state whether it is a loopback state and terminating the search with success if a loopback state is found;

e) checking for each j th state before the start state whether it is a loopback state and terminating the search with success if a loopback state is found;

f) continuing the search by increasing i until the said time frame bound is reached and repeating steps a-e;

g) terminating the search inconclusively if the said time frame bound is reached.

11. The method of claim 10 wherein step d is performed by:

(di) checking satisfiability of a transition from the i th state to the j th state,

(dii) if the transition of step di is satisfiable, terminating the search with success,

(diii) if the transition of step di unsatisfiable, learning that such a transition does not exist and adding this knowledge to the constraint database,

(div) continuing the search by repeating (di)-(diii) until all states from the said start state to the i th state have been examined.

12. The method of claim 10 wherein step e is performed by:

(ei) checking for satisfiability of p at each state from the j th state up to a start state,

(eii) if unsatisfiable in step ei, quitting Step e and moving to Step f,

(eiii) if satisfiable in step ei, checking satisfiability of a transition from the i th state to the j th state,

(eiv) if the said transition of step eiii is satisfiable, terminating the search with success,

(ev) if the said transition of step eiii is unsatisfiable, continuing the search by repeating Steps ei-eiv until all states from the initial state of the circuit up to the start state have been examined.

13. The method of claim 10 further comprising checking for completeness of a solution between steps e and f, to determine failure wherein, failure characterizes that success in step e is not achievable for any time frame i.

14. The method of claim 13 wherein the checking for completeness further comprises:

(i) adding constraints to ensure that same states are not revisited in the said path, and checking satisfiability of the constraint database,

(ii) if unsatisfiable in step i, terminating the search with the said failure,

(iii) if satisfiable in step i, continuing search; and

(iv) repeating steps i-iii until all previous states have been examined.

15. The method of claim 10 , wherein a subset of satisfiability checks is combined into a single satisfiability check.

16. The method in claim 1 wherein the property checking schema for the said LTL operator U(p, q) for a given time frame bound comprises:

a) starting search from a given start state at time frame i with a given constraint database, wherein i=0 corresponds to an initial state;

b) checking for satisfiability of q in the i th state of a path,

c) if satisfiable, terminating the search with success;

d) if unsatisfiable, learning that q is always false in the i th state and adding this knowledge to the constraint database;

e) adding the constraint to the database to ensure that p is satisfied in the i th state, and checking for satisfiability;

f) if unsatisfiable in step e, terminating the search with failure;

g) if satisfiable in step e, continuing the search;

h) continuing the search by increasing i until the said time frame bound is reached and repeating steps b-g; and

i) terminating the search inconclusively if the said time frame bound is reached.

17. The method of claim 16 further comprising checking for completeness of the solution between steps g and h, to determine failure, wherein failure characterizes that the success in step c is not achievable for any time frame i.

18. The method of claim 17 , wherein the checking for completeness further comprises:

(i) adding constraints to ensure that same states are not revisited in the said path, and checking satisfiability of the constraint database;

(ii) if unsatisfiable in step i, terminating the search with the said failure;

(iii) if satisfiable in step i, continuing search; and

(iv) repeating steps i-iii until all previous states have been examined.

19. The method of claim 16 , wherein a subset of satisfiability checks is combined into a single satisfiability check.

20. The method in claim 1 wherein the property checking schema for the said LTL operator X(p) comprises:

a) starting search from a start state at time frame i with a given constraint database, where i=0 corresponds to an initial state of the circuit;

b) checking for satisfiability of p in the next state, wherein next state characterizes the state reachable next from the initial state,

c) terminating with success if p is found true in the next state, d) terminating with failure if p is found false in the next state,

e) terminating inconclusively if check for p is inconclusive in the next state.

21. The method of claim 20 , wherein a subset of satisfiability checks is combined into a single satisfiability check.