UTILIZING AN UNSAT PROOF FOR MODEL CHECKING

• US 20110010139A1
• Filed: 07/13/2009
• Published: 01/13/2011
• Est. Priority Date: 07/13/2009
• Status: Active Grant

• Current Assignee: GlobalFoundries, Inc.
• Original Assignee: International Business Machines Corporation
• Inventors: Hoory, Shlomo, Shacham, Ohad, Fuhrmann, Oded
• Granted Patent: US 8,161,433 B2
• Time in Patent Office: Days
• US Class Current: 703/2
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A proof of unsatisfiability associated with a bounded model may be extended to apply to another bounded model having a larger bound. In some exemplary embodiments, an unbounded model may be proved using one or more such extensions. A proof may be reordered in order to decrease its size and increase the productivity of systems that utilize it. The proof may be reorder by a natural temporal order of cycles.

Claims

1. A computerized system comprising:

a processor;

an interface for receiving a proof of a conclusion associated with a CNF formula;

the CNF formula representing a model and a specification property in a predetermined number of cycles;

the proof comprising an initial axiom clause, a transition axiom clause and a deduction clause; and

an invariant extractor module for identifying an invariant in the proof;

the invariant is a portion of the proof;

said invariant extractor module utilizes said processor for identifying the invariant.

2. The computerized system of claim 1 wherein:

the proof of a conclusion is a proof of unsatisfiability;

said invariant extractor module further comprises a delta shifter module;

said delta shifter module receives a first clause associated with a first cycle and a predetermined number of cycles and determines a second clause associated with a second cycle;

the second clause is substantially equivalent to the first clause;

the difference between the first cycle and the second cycle is the predetermined number of cycles.

3. The computerized system of claim 2 wherein:

said invariant extractor module further comprises a proof visitor module for traversing the proof of unsatisfiability;

said proof visitor comprises a set of one or more visited clauses;

said proof visitor module utilizes said delta shifter module to determine whether the set of one or more visited clauses comprises a first clause that is substantial equivalent to a second clause.

4. The computerized system of claim 3 wherein:

said invariant extractor module further comprising a node identifier module for identifying an initial axiom clause, a transition axiom clause and a deduction clause.

5. The computerized system of claim 4 wherein:

said invariant extractor module further comprises a delta chooser module for determining a predetermined number of cycles;

the predetermined number of cycles is utilized by said delta shifter.

6. The computerized system of claim 5 further comprising:

a CNF formula constructor for determining the CNF formula based on the model and the specification property.

7. The computerized system of claim 6 further comprising:

a SAT solver for determining unsatisfiability of the CNF formula.

8. The computerized system of claim 6 wherein said invariant extractor module is configured to extract an invariant from the proof of unsatisfiability.

9. The computerized system of claim 1 wherein

said invariant extractor module further comprises a proof reordering module for reordering the proof.

10. The computerized system of claim 6 wherein the proof is a proof of unsatisfiability;

said proof reordering module is a temporal proof reordering module;

said temporal proof reordering module is configured to reorder the proof of unsatisfiability in respect to a temporal consideration.

11. A method comprising:

obtaining a proof of a conclusion associated with a CNF formula;

the CNF formula representing a model and a specification property in a first predetermined number of cycles;

the proof comprising an initial axiom clause, a transition axiom clause and a deduction clause;

identifying an invariant in the proof;

said identifying an invariant in the proof is performed by a processor; and

determining the specification property holds for the model in a second predetermined number of cycles based on the invariant;

whereby the proof of the conclusion associated with the CNF formula is transformed to provide a proof of the conclusion associated with an extended CNF formula representing the model and the specification property in the second predetermined number of cycles.

12. The method of claim 11 wherein said identifying an invariant in the proof comprises:

traversing the proof and collecting a set of visited clauses;

the set of visited clauses comprises transition axiom clauses and deduction clauses.

13. The method of claim 12 wherein said traversing the proof further comprising:

determining a first clause associated with a first cycle that is substantially equivalent to a second clause associated with a second cycle;

the different between the first cycle and the second cycle is a predetermined number of cycles.

14. The method of claim 12 wherein said identifying an invariant in the proof comprises identifying a delta invariant in the proof.

15. The method of claim 14 wherein identifying a delta invariant in the proof is performed iteratively until a delta invariant is identified.

16. The method of claim 14 further comprising:

determining the specification property holds for the model in another number of cycles based on the delta invariant.

17. The method of claim 14 further comprising iteratively identifying a delta invariant in the proof until the specification property is determined to hold for the model in an unbounded number of cycles.

18. The method of claim 14 further comprises reordering the proof.

19. The method of claim 18 wherein reordering the proof comprising determining a clause is associated with a cycle;

and reordering the proof based on an order of cycles.

20. The method of claim 11 further comprising:

extracting the invariant identified in said identifying an invariant in the proof; and

wherein said determining the specification property holds for the model in a second predetermined number of cycles based on the invariant comprises determining a second CNF formula associated with the model;

the second CNF formula comprises an invariant clause and a transition axiom clause;

the invariant clause is associated with the invariant.

21. The method of claim 20 wherein the second CNF formula further comprising an init axiom clause.

22. A computer program product comprising:

a computer readable medium;

first program instruction for obtaining a proof of a conclusion associated with a CNF formula;

the CNF formula representing a model and a specification property in a first predetermined number of cycles;

the proof comprising an initial axiom clause, a transition axiom clause and a deduction clause;

second program instruction for identifying an invariant in the proof;

said identifying an invariant in the proof is performed by a processor; and

third program instruction for determining the specification property holds for the model in a second predetermined number of cycles based on the invariant

wherein said first, second, and third program instructions are stored on said computer readable media.