Simulation-based functional verification of microcircuit designs

• US 7,130,783 B1
• Filed: 01/12/2001
• Issued: 10/31/2006
• Est. Priority Date: 01/12/2001
• Status: Active Grant

• Current Assignee: Synopsys Incorporated
• Original Assignee: Synopsys Incorporated
• Inventors: Ho, Pei-Hsin, Harer, Kevin M., Damiano, Robert F
• Primary Examiner(s): Rodriguez, Paul L.
• Assistant Examiner(s): STEVENS, THOMAS H
• Application Number:
  US09/760,063
• Time in Patent Office: 2,118 Days
• Field of Search: 703/13, 703/14, 716/5, 716/4, 717/106, 717/104
• US Class Current: 703/13
• CPC Class Codes: G06F 11/261 by simulating additional hardware, e.g. fault simulation
• CPC Class Codes: G06F 30/33 Design verification, e.g. functional simulation or model checking
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

System, methods, and apparatus for verifying microcircuit designs by interleaving between random and formal simulation techniques to identify input traces useful for driving designs under test into sequences of device states. In a method aspect the invention provides process for beginning random simulation of a sequence of states of a microcircuit design by inputting a sequence of random input vectors to a design under test model in order to obtain a sequence of random simulation states; monitoring a simulation coverage progress metric to determine a preference for switching from random simulation to formal methods of simulating states in the design under test; beginning formal simulation of states in the design under test and monitoring a formal coverage progress metric to determine a preference for resuming random simulation of states of said microcircuit design; and resuming random simulation. Preferably the process of interleaving simulation methods continues until an input vector suitable for driving the design under test model into each of a set of previously-identified goal states has been obtained.

Claims

1. A method of verifying a design for a microcircuit, the method comprising:

beginning random simulation of a sequence of states of a microcircuit design by inputting a sequence of random input vectors to a random simulation model to obtain a sequence of random simulation states;

monitoring a simulation coverage progress metric to determine on a basis of said sequence of random simulation states a preference for beginning formal simulation of a sequence of states of said microcircuit design;

beginning formal simulation of a sequence of states of said microcircuit design by using formal simulation methods to simulate a sequence of formal simulation states in a formal simulation model of said microcircuit design;

monitoring a formal coverage progress metric to determine on a basis of said sequence of formal simulation states a preference for resuming random simulation of states of said microcircuit design;

resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design caused by inputting said random input vector sequence to said random simulation model;

testing for whether a goal state has been reached; and

recording an indication that a goal state has been reached, that can be used by a user, if a goal state has been found.

2. The method of claim 1, wherein said random simulation model and said formal simulation model are the same.

3. The method of claim 1, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation.

4. The method of claim 1, wherein said simulating a sequence of formal simulation states comprises the use of satisfiability techniques.

5. The method of claim 1, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation and satisfiability techniques.

6. The method of claim 1, wherein said beginning of formal simulation is initiated by simulating in said formal simulation model a state of said microcircuit design previously simulated by inputting at least a portion of said random input vector sequence to said random simulation model.

7. The method of claim 1, further comprising proving at least one of a set of previously-defined goal states of said microcircuit design unreachable.

8. The method of claim 1, wherein said process of monitoring said simulation coverage progress metric, beginning formal simulation, monitoring said formal coverage progress metric, and resuming said random simulation is continued until a previously-defined set of goal states of said microcircuit design are simulated or proved not reachable.

33. The method of claim 1, wherein:

said beginning of said formal simulation of a sequence of states is initiated from a start state;

said formal simulation of a sequence of states of said microcircuit design comprises simulating a state defined as a goal state; and

resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design comprises simulating in said random simulation model a sequence of states simulated in said formal simulation model, starting with said start state and comprising said goal state.

9. A method of verifying a design for a microcircuit, the method performed by a data processing system and comprising:

beginning random simulation of a sequence of states of a microcircuit design by inputting a sequence of random input vectors to a random simulation model to obtain a sequence of random simulation states;

monitoring a simulation coverage progress metric to determine on a basis of said sequence of random simulation states a preference for beginning formal simulation of a sequence of states of said microcircuit design;

beginning formal simulation of a sequence of states of said microcircuit design by using formal simulation methods to simulate a sequence of formal simulation states in a formal simulation model of said microcircuit design;

monitoring a formal coverage progress metric to determine on a basis of said sequence of formal simulation states a preference for resuming random simulation of states of said microcircuit design;

resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design caused by inputting said random input vector sequence to said random simulation model;

testing for whether a goal state has been reached; and

recording an indication that a goal state has been reached, that can be used by a user, if a coal state has been found.

10. The method of claim 9, wherein said random simulation model and said formal simulation model are the same.

11. The method of claim 9, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation.

12. The method of claim 9, wherein said simulating a sequence of formal simulation states comprises the use of satisfiability techniques.

13. The method of claim 9, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation and satisfiability techniques.

14. The method of claim 9, wherein said beginning of formal simulation is initiated by simulating in said formal simulation model a state of said microcircuit design previously simulated by inputting at least a portion of said random input vector sequence to said random simulation model.

15. The method of claim 9, further comprising proving at least one of a set of previously-defined goal states of said microcircuit design unreachable.

16. The method of claim 9, wherein said process of monitoring said simulation coverage progress metric, beginning formal simulation, monitoring said formal coverage progress metric, and resuming said random simulation is continued until a previously-defined set of goal states of said microcircuit design are simulated or proved not reachable.

34. The method of claim 9, wherein:

said beginning of said formal simulation of a sequence of states is initiated from a start state;

said formal simulation of a sequence of states of said microcircuit design comprises simulating a state defined as a goal state; and

resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design comprises simulating in said random simulation model a sequence of states simulated in said formal simulation model, starting with said start state and comprising said goal state.

17. A data processing system for verifying a design for a microcircuit, the system comprising:

a circuit configured for random simulation of a sequence of states of a microcircuit design by inputting a sequence of random input vectors to a random simulation model to obtain a sequence of random simulation states;

a circuit configured for monitoring a simulation coverage progress metric to determine on a basis of said sequence of random simulation states a preference for beginning formal simulation of a sequence of states of said microcircuit design;

a circuit configured for beginning formal simulation of a sequence of states of said microcircuit design by using formal simulation methods to simulate a sequence of formal simulation states in a formal simulation model of said microcircuit design;

a circuit configured for monitoring a formal coverage progress metric to determine on a basis of said sequence of formal simulation states a preference for resuming random simulation of states of said microcircuit design;

a circuit configured for resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design caused by inputting said random input vector sequence to said random simulation model;

a circuit configured for testing for whether a goal state has been reached; and

a circuit configured for recording an indication that a goal state has been reached, that can be used by a user, if a goal state has been found.

18. The system of claim 17, wherein said random simulation model and said formal simulation model are the same.

19. The system of claim 17, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation.

20. The system of claim 17, wherein said simulating a sequence of formal simulation states comprises the use of satisfiability techniques.

21. The system of claim 17, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation and satisfiability techniques.

22. The system of claim 17, wherein said beginning of formal simulation is initiated by simulating in said formal simulation model a state of said microcircuit design previously simulated by inputting at least a portion of said random input vector sequence to said random simulation model.

23. The system of claim 17, further comprising a circuit configured for proving at least one of a set of previously-defined goal states of said microcircuit design unreachable.

24. The system of claim 17, wherein said circuits are configured such that said process of monitoring said simulation coverage progress metric, beginning formal simulation, monitoring said formal coverage progress metric, and resuming said random simulation is continued until a previously-defined set of goal states of said microcircuit design are simulated or proved not reachable.

35. The system of claim 17, wherein:

said beginning of said formal simulation of a sequence of states is initiated from a start state;

said formal simulation of a sequence of states of said microcircuit design comprises simulating a state defined as a goal state; and

resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design comprises simulating in said random simulation model a sequence of states simulated in said formal simulation model, starting with said start state and comprising said goal state.

25. A computer program product comprising a computer usable medium having computer readable code embodied therein for verifying a design for a microcircuit, the computer program product comprising:

computer readable program code devices configured to cause a computer to effect random simulation of a sequence of states of a microcircuit design by inputting a sequence of random input vectors to a random simulation model to obtain a sequence of random simulation states;

computer readable program code devices configured to cause a computer to effect monitoring of a simulation coverage progress metric to determine on a basis of said sequence of random simulation states a preference for beginning formal simulation of a sequence of states of said microcircuit design;

computer readable program code devices configured to cause a computer to effect beginning formal simulation of a sequence of states of said microcircuit design by using formal simulation methods to simulate a sequence of formal simulation states in a formal simulation model of said microcircuit design;

computer readable program code devices configured to cause a computer to effect monitoring a formal coverage progress metric to determine on a basis of said sequence of formal simulation states a preference for resuming random simulation of states of said microcircuit design;

computer readable program code devices configured to cause a computer to effect resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design caused by inputting said random input vector sequence to said random simulation model;

computer readable program code devices configured to cause a computer to effect testing for whether a goal state has been reached; and

computer readable program code devices configured to cause a computer to effect recording an indication that a goal state has been reached, that can be used by a user, if a goal state has been found.

26. The product of claim 25, wherein said random simulation model and said formal simulation model are the same.

27. The product of claim 25, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation.

28. The product of claim 25, wherein said simulating a sequence of formal simulation states comprises the use of satisfiability techniques.

29. The product of claim 25, wherein said simulating a sequence of formal simulation states comprises the use of symbolic simulation and satisfiability techniques.

30. The product of claim 25, wherein said beginning of formal simulation is initiated by simulating in said formal simulation model a state of said microcircuit design previously simulated by inputting at least a portion of said random input vector sequence to said random simulation model.

31. The product of claim 25, further comprising proving at least one of a set of previously-defined goal states of said microcircuit design unreachable.

32. The product of claim 25, wherein said process of monitoring said simulation coverage progress metric, beginning formal simulation, monitoring said formal coverage progress metric, and resuming said random simulation is continued until a previously-defined set of goal states of said microcircuit design are simulated or proved unreachable.

36. The product of claim 25, wherein:

said beginning of said formal simulation of a sequence of states is initiated from a start state;

said formal simulation of a sequence of states of said microcircuit design comprises simulating a state defined as a goal state; and

resuming generation of random input vector sequences for said random simulation model of a microcircuit design and said simulating of a sequence of random simulation states of said microcircuit design comprises simulating in said random simulation model a sequence of states simulated in said formal simulation model, starting with said start state and comprising said goal state.