Property specific testbench generation framework for circuit design validation by guided simulation

• US 6,975,976 B1
• Filed: 10/23/2000
• Issued: 12/13/2005
• Est. Priority Date: 03/20/2000
• Status: Expired due to Fees

• Current Assignee: NEC Corporation
• Original Assignee: NEC Corporation
• Inventors: Casavant, Albert E., Gupta, Aarti, Ashar, Pranav
• Primary Examiner(s): Follansbee, John
• Assistant Examiner(s): PEREZ DAPLE, AARON C
• Application Number:
  US09/693,976
• Time in Patent Office: 1,877 Days
• Field of Search: 703 14- 16, 703/21, 716/4
• US Class Current: 703/14
• CPC Class Codes: G01R 31/318314 Tools, e.g. program interfaces, test suite, test bench, simulation hardware, test compiler, test program languages simulation software G01R31/318357; emulators G06F11/261
• CPC Class Codes: G01R 31/318357 Simulation computer simulation of digital circuits G06F30/3308
• CPC Class Codes: G01R 31/318364 as a result of hardware simulation, e.g. in an HDL environment computer-aided simulation of circuits G06F30/3308
• CPC Class Codes: G06F 30/33 Design verification, e.g. functional simulation or model checking

Abstract

Simulation continues to be the primary technique for functional validation of designs. It is important that simulation vectors be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The focus of this work is to generate property-specific testbenches that are targeted either at proving the correctness of a property or at finding a bug. It is based on performing property-specific analysis on iteratively less abstract models of the design in order to obtain interesting paths in the form of a Witness Graph, which is then targeted during simulation of the entire design. This testbench generation framework will form an integral part of a comprehensive verification system currently being developed.

Claims

1. A method of verification for a design, comprising:

providing a description of said design;

specifying correctness criteria for said design, wherein said correctness criteria are expressed as one or more correctness properties;

abstracting said design description to provide an abstract model of said design;

generating a witness graph for said one or more correctness properties based on a deterministic analysis of said abstract model where the deterministic analysis serves to modify the abstract model by iteratively refining and pruning states and transitions which capture all witnesses or counterexamples demonstrating said one or more correctness properties; and

when the deterministic analysis does not produce a conclusive result, generating a testbench automatically from said witness graph for performing simulation with said testbench, where the testbench generates simulation test vectors for the simulation that target states and transitions in the witness graph when searching for a concrete witness or counterexample with respect to said correctness criteria.

2. The method for verification as set forth in claim 1, wherein:

said generation of said testbench comprises;

determining embedded constraints for guiding vector generation based on said witness graph;

determining priorities for guiding said vector generation based on said witness graph;

generating a vector generator module including said embedded constraints and said priorities; and

generating a monitor module, said monitor module checking said conclusive result;

said simulation of said design, using said generated test bench, comprises;

generating said vectors with said vector generator module based on said embedded constraints, including generating random patterns and using said constraints as a filter to select desirable ones of said random patterns; and

checking said monitor module for property violation or satisfaction.

3. The method of verification as set forth in claim 2, wherein:

said embedded constraints are derived from transition conditions in said witness graph; and

said priorities are associated with transitions in said witness graph.

4. The method of verification as set forth in claim 3, wherein:

said priorities are generated from said witness graph based on one or more of;

distance to targets;

transition probabilities; and

simulation trace data.

5. The method of verification as set forth in claim 1, wherein:

said generation of said witness graph comprises;

removing a portion from said design when an influence determination does not indicate that said portion of said design is in a cone of influence of said property;

modeling, as an initial abstract model, a controller state and variables in a datapath state directly involved in predicates of said correctness property;

performing deterministic analysis on said abstract model; and

pruning said abstract model to obtain said witness graph;

said influence determination indicates said portion of said design is in said cone of influence of said property when said portion of said design is one or more of;

a portion directly affecting said variables in said predicates of said property; and

a portion affecting branching which in turn affects predicates of said property;

said deterministic analysis determines which portion in said abstract model indicates paths relating to said conclusive result for said property;

said pruning comprises removing a portion in said abstract model indicated by said analysis not to relate to said conclusive result for said property.

6. The method of verification as set forth in claim 5, wherein:

said pruning is followed by a step of refining said abstract model by adding variables from said datapath state to provide a refined abstract model;

said analysis, pruning, and refining steps are performed in an iterative process; and

said witness graph is said refined abstract model at the end of said iterative process.

7. The method of verification as set forth in claim 5, wherein said property is represented using a computation tree logic (CTL) formula.

8. The method of verification as set forth in claim 7, wherein said step of analysis is performed by:

determining CTL subformulas of said CTL formula;

with each of said CTL subformulas, associating a given set of abstract states corresponding to an over-approximate set of concrete states satisfying said CTL subformula, said given set of abstract states defining an upper set;

for ones of said CTL subformulas beginning with an E-type operator, performing standard model checking over said abstract model;

for ones of said CTL subformulas beginning with an A-type operator;

selecting an E-type operator corresponding to said A-type operator and guaranteed to result in an over-approximation; and

computing an other set of abstract states, corresponding to an intersection of said upper set with a set recursively computed for the negation of said A-type operator, said other set of abstract states defining a negative set;

checking an initial state of the design to determine a conclusive result, wherein;

when said initial state does not belong to said upper set, determining said property to be conclusively proved to be false;

when said property represented using said CTL formula starts with said A-type operator, and when said initial state belongs to said upper set, and when said initial state does not belong to said negative set, determining said property to conclusively proved to be true; and

determining said analysis to be inconclusive when said property is not conclusively to be proved to be one of true and false.

9. The method of verification as set forth in claim 8, wherein said step of pruning comprises:

marking witness states; and

then

pruning unmarked states by replacement with a sink state having every transition therefrom leading to said sink state, and all atomic propositions in said sink state being assumed false.

10. The method of verification as set forth in claim 9, wherein said step of marking said witness states comprises:

computing a witness-top set of states consisting of the intersection of set of states reachable from initial state of said design and said upper set;

marking all of said witness-top set of states;

using a marking procedure, for each of said CTL subformulas of said CTL formula representing said property, with said witness-top set defining a care set, comprising the steps of;

associating with said CTL subformula, as a witness set thereof, a given set of states defined by the intersection of said upper set associated with said CTL subformula and said care set;

for ones of said CTL subformulas beginning with said EX operator;

marking additional states in the image of said witness set; and

recursively applying said marking procedure to the CTL subformulas thereof, beginning with said EX operator, with said additional states as said care set;

for ones of said CTL subformulas beginning with an A-type operator;

determining a neg-witness set as the intersection of said negative set associated with said A-type subformula and said care set; and

recursively applying said marking procedure on the negation of said A-type subformula, with said neg-witness set as said care set; and

for all other types of said CTL subformulas, applying said marking procedure recursively on the CTL subformulas thereof, with said witness set as said care set.

11. The method of verification as set forth in claim 10, wherein said vector generator module is generated to include a search of said witness and neg-witness sets of states for a concrete witness, returning an indication of success when finding said concrete witness.

12. The method of verification as set forth in claim 11, wherein said search is conducted suing a backtracking method comprising:

specifying a CTL formula;

specifying a given concrete state belonging to said witness set associated with said CTL formula;

starting from said concrete state;

determining an indication of success when there exists a concrete witness for said CTL formula, and failure otherwise; and

backtracking when said indication is failure, wherein;

when said CTL operator is not an A-type operator, search subproblems are conducted on the subformulas of said CTL subformula and each concrete state belonging to the associated witness sets;

when said CTL operator is an A-type operator and said state does not belong to said negative set, said indication is success;

when said CTL operator is an A-type operator and when said state belongs to said negative set, a search subproblem is set up with the negation of said CTL formula and said concrete state, wherein success of said negated subproblem indicates failure, and failure of said negated subproblem indicates success.

13. The method of verification as set forth in claim 12, wherein:

said search subproblems on said CTL subformulas and said concrete states belonging to the associated witness sets are set up in a prioritized manner based on one or more of;

distance to targets,

transition probabilities, and

simulator trace data.

14. The method for verification as set forth in claim 1, wherein said deterministic analysis comprises using symbolic model checking on the abstract model to identify states and transitions which capture all witnesses or counterexamples demonstrating the correctness properties.

15. The method for verification as set forth claim 14, wherein said model checking further comprises:

determining sub-properties for said one or more correctness properties;

for each sub-property that can be represented with an operator applying to all paths in the abstract model, computing a negative set which is an intersection of states and transitions in the abstract model which satisfy a negation of the sub-property and states and transitions in the abstract model which satisfy an over-approximation of the sub-property, such that the negative set can be used to identify states and transitions which capture witnesses or counterexamples for the sub-property.

16. The method for verification as set forth in claim 15, wherein said one or more correctness properties are represented using a Computation Tree Logic (CTL) formula and wherein the sub-properties are CTL subformulas.

17. The method for verification as set forth in claim 16, wherein the operator applying to all paths in the abstract model is an A-type operator.

18. The method for verification as set forth in claim 16, wherein the operator applying to some paths in the abstract model is an E-type operator.

19. The method for verification as set forth in claim 1, wherein said deterministic analysis comprises using constraint solving on the abstract model to identify states and transitions which capture all witnesses or counterexamples demonstrating said one or more correctness properties.

20. The method for verification as set forth in claim 1, wherein the step of generating the witness graph further comprises the steps of:

refining the modified abstract model for the deterministic analysis by selectively bringing back datapath variables into the abstract model; and

using the deterministic analysis to prune the modified abstract model by removing states which cannot serve as either a witness or counter-example for said one or more correctness properties.

21. The method for verification as set forth in claim 20, wherein the steps of refining and pruning are iterated until a limit on resources is reached.

22. The method for verification as set forth in claim 1, wherein the testbench prioritizes the simulation search for said concrete witnesses or counterexamples based on said witness graph.

23. A method of assessing simulation coverage of a given set of simulation vectors for a given design, comprising:

providing a description of said design;

specifying correctness criteria for said design, wherein said correctness criteria are expressed as one or more correctness properties;

generating a witness graph for one or more of said correctness properties; and

determining coverage of said witness graph, using said given set of simulation vectors, by marking entities visited by said given set of simulation vectors in said witness graph, said entities being selected from the set consisting of states, transitions, and paths;

wherein said generation of said witness graph comprises;

removing a portion from said design when an influence determination does not indicate that said portion of said design is in a cone of influence of said property;

modeling, as an initial abstract model, a controller state and variables in a datapath state directly involved in predicates of said correctness property;

performing deterministic analysis on said abstract model; and

pruning said abstract model to obtain said witness graph;

said influence determination indicates said portion of said design is in said cone of influence of said property when said portion of said design is one or more of;

a portion directly affecting said variables in said predicates of said property; and

a portion affecting branching which in turn affects predicates of said property;

said deterministic analysis determines which portion in said abstract model indicates paths relating to said conclusive result for said property; and

said pruning comprises removing a portion in said abstract model indicated by said analysis not to relate to said conclusive result for said property.

24. A device-readable medium comprising program instructions for causing the device to perform verification for a design, comprising:

receiving an abstract model of said design, said abstract model abstracted from a design description of said design;

receiving one or more correctness properties representing correctness criteria specified for said design;

generating a witness graph for said one or more correctness properties based on a deterministic analysis of said abstract model where the deterministic analysis serves to modify the abstract model by iteratively refining and pruning states and transitions which capture all witnesses or counterexamples demonstrating said one or more correctness properties; and

when the deterministic analysis does not produce a conclusive result, automatically generating a testbench from said witness graph for performing simulation with said testbench, where the testbench generates simulation test vectors for the simulation that target states and transitions in the witness graph when searching for a concrete witness or counterexample with respect to said correctness criteria.

25. The device-readable medium as set forth in claim 24, wherein said deterministic analysis comprises using symbolic model checking on the abstract model to identify states and transitions which capture all witnesses or counterexamples demonstrating the correctness properties.

26. The device-readable medium as set forth in claim 25, wherein said model checking further comprises:

determining sub-properties for said one or more correctness properties;

for each sub-property that can be represented with an operator applying to all paths in the abstract model, computing a negative set which is an intersection of states and transitions in the abstract model which satisfy a negation of the sub-property and states and transitions in the abstract model which satisfy an over-approximation of the sub-property, such that the negative set can be used to identify states and transitions which capture witnesses or counterexamples for the sub-property.

27. The device-readable medium as set forth in claim 26, wherein said one or more correctness properties are represented using a Computation Tree Logic (CTL) formula and wherein the sub-properties are CTL subformulas.

28. The device-readable medium as set forth in claim 27, wherein the operator applying to all paths in the abstract model is an A-type operator.

29. The device-readable medium as set forth in claim 27, wherein the operator applying to some paths in the abstract model is an E-type operator.

30. The device-readable medium as set forth in claim 24, wherein said deterministic analysis comprises using constraint solving on the abstract model to identify states and transitions which capture all witnesses or counterexamples demonstrating said one or more correctness properties.

31. The device-readable medium as set forth in claim 24, wherein the step of generating the witness graph further comprises the steps of:

refining the modified abstract model for the deterministic analysis by selectively bringing back datapath variables into the abstract model; and

using the deterministic analysis to prune the modified abstract model by removing states which cannot serve as either a witness or counter-example for the correctness properties.

32. The device-readable medium as set forth in claim 31, wherein the steps of refining and pruning are iterated until a limit on resources is reached.

33. The device-readable medium as set forth in claim 24, wherein the testbench prioritizes the simulation search for said concrete witnesses or counterexamples based on said witness graph.

37. The apparatus as set forth in claim 26, wherein said correctness properties are represented using a Computation Tree Logic (CTL) formula and wherein the sub-properties are CTL subformulas.

38. The apparatus as set forth in claim 37, wherein the operator applying to all paths in the abstract model is an A-type operator.

39. The apparatus as set forth in claim 37, wherein the operator applying to some paths in the abstract model is an E-type operator.

34. An apparatus for verification of a design comprising:

an input module for receiving an abstract model of said design, said abstract model abstracted from a design description of said design, and for receiving one or more correctness properties representing correctness criteria specified for said design;

a witness graph module for generating a witness graph for said one or more correctness properties based on a deterministic analysis of said abstract model when the deterministic analysis serves to modify the abstract model by iteratively refining and pruning states and transitions which capture all witnesses or counterexamples demonstrating the correctness properties; and

a testbench module for generating a testbench automatically from said witness graph for performing simulation with said testbench, where the testbench generates simulation test vectors for the simulation that target states and transitions in the witness graph when searching for a concrete witness or counterexample with respect to said correctness criteria.

35. The apparatus as set forth in claim 34, wherein said deterministic analysis comprises using symbolic model checking on the abstract model to identify states and transitions which capture all witnesses or counterexamples demonstrating the correctness properties.

36. The apparatus as set forth in claim 35, wherein said model checking further comprises:

determining sub-properties for said correctness properties;

for each sub-property that can be represented with an operator applying to all paths in the abstract model, computing a negative set which is an intersection of states and transitions in the abstract model which satisfy a negation of the sub-property and states and transitions in the abstract model which satisfy an over-approximation of the sub-property, such that the negative set can be used to identify states and transitions which capture witnesses or counterexamples for the sub-property.

40. The apparatus as set forth in claim 34, wherein said deterministic analysis comprises using constraint solving on the abstract model to identify states and transitions which capture all witnesses or counterexamples demonstrating the correctness properties.

41. The apparatus as set forth in claim 34, wherein said generating the witness graph further comprises:

refining the modified abstract model for the deterministic analysis by selectively bringing back datapath variables into the abstract model; and

using the deterministic analysis to prune the modified abstract model by removing states which cannot serve as either a witness or counter-example for the correctness properties.

42. The apparatus as set forth in claim 41, wherein the steps of refining and pruning are iterated until a limit on resources is reached.

43. The apparatus as set forth in claim 34, wherein the testbench prioritizes the simulation search for said concrete witnesses or counterexamples based on said witness graph.