Design verification device, method and memory media for integrated circuits

• US 6,449,750 B1
• Filed: 01/14/2000
• Issued: 09/10/2002
• Est. Priority Date: 01/18/1999
• Status: Expired due to Fees

• Current Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Original Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Inventors: Tsuchiya, Takehiko
• Primary Examiner(s): Smith, Matthew
• Assistant Examiner(s): LEE, GRANVILL D
• Application Number:
  US09/482,935
• Time in Patent Office: 970 Days
• Field of Search: 716/18, 716/3, 716/5-6, 716/17, 716/11, 716/4, 714/724
• US Class Current: 716/107
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

To provide a design verification device, a method and a memory medium therefor, for a semiconductor integrated circuit, capable of effectively introducing the formal verification in a higher-level design and capable of constructing a high-speed function verification environment with high verification assurance. A design verification device, a method and a memory medium therefor, for a semiconductor integrated circuit, has a function verification system which has an input of a circuit description before an alteration and a circuit description after the alteration and identifies an altered portion according to a disagreed portion, wherein formal verification is carried out for a circuit description that can assure an agreement with a key point corresponding to an output of a register and an input and an output of a signal in the circuit descriptions before and after the alteration, and verification is carried out by utilizing an event-driven simulation for a circuit description that cannot assure an agreement or equivalence of the key point.

Claims

1. A design verification device for a semiconductor integrated circuit, the device comprising:

a mechanism for identifying an altered portion according to a disagreed portion of a circuit description from input means for inputting the circuit description before an alteration and a circuit description after the alteration; and

verification means including (i) means for determining portions of the circuit description, which correspond to an output of each of registers, an external input to the circuit description and an output from the circuit description, as key points, and (ii) means for cutting out a logic connected between each of the key points and a preceding key point, as a logic circuit group, said verification means being used for carrying out formal verification for the logic circuit group that can assure an agreement or equivalence of the key point in the circuit descriptions before and after the alteration, and for carrying out verification by utilizing an event-driven simulation for the logic circuit group that cannot assure an agreement or equivalence of the key point to the circuit descriptions before and the after the alteration.

2. A design verification device according to claim 1, further comprising:

a function of inputting expectation values relating to the circuit descriptions before and after the alteration in the verification means by simulation; and

comparing and determining means for comparing actual results of simulation from the verification means by simulation with the expectation values.

3. A design verification device according to claim 2, wherein the comparing and determining means compares a test vector for which a disagreement has occurred and an output according to the circuit descriptions before and after the alteration using this test vector with the expectation values, based on the actual results of simulation from the verification means by simulation, thereby to determine whether an alteration according to the expectation has been made or not.

4. A design verification device according to claim 2, wherein the expectation values are prepared by specifying art altered portion of a circuit before and after the alteration in the circuit description stage of a register transfer level, thereby to analyze the circuit description thereof, and by obtaining a test vector for which results of execution are different between before and after the alteration as well as results of the execution thereof, or by inputting a test vector and results of the execution thereof from a wave form indicated by a graphical user interface.

5. A design verification device according to claim 2, further comprising a function of registering as new expectation values an output of the circuit portion relating to the circuit descriptions before and after the alteration using the test vector for which the disagreed portion has occurred, thereby to make it possible to continue the event-driven simulation.

6. A design verification device for a semiconductor integrated circuit, the device comprising:

means for determining portions of the circuit description, which correspond to an output of each of registers, an external input to the circuit description and an output from the circuit description, as key points;

means for cutting out a logic connected between each of the key points and a preceding key point, as a logic circuit group;

means for identifying an altered portion for mapping the key point in the circuit descriptions before an alteration and after the alteration, setting as an external input and output a key point of which descriptions before and after the alteration agree with each other, said key point being closest to a disagreed portion between the circuit descriptions before and after the alteration, and modularizing a circuit portion including the altered portion,

verification means by simulation for verifying the modularized circuit portion in the circuit descriptions before and after the alteration respectively by utilizing an event-driven simulation; and

means for formal verification for verifying the logic circuit group except for the modularized circuit by utilizing formal verification for the circuit descriptions before and after the alteration respectively by reflecting only a node that has been regarded as the external input and output.

7. A design verification device according to claim 6, wherein the means for formal verification has a function of assuming that there is a logically altered portion in the circuit descriptions before and after the alteration, when a logical disagreement occurred, and regarding as external input and output the input to and output from a logic cone including a node that has been regarded as the external input and output and the logically altered portion out of logic cones following the formal verification, thereby to cut out and modularize the circuit description including the logically altered;

and, the verification means by simulation verifies each modularized circuit portion in the circuit descriptions before and after the alteration.

8. A design verification device according to claim 6, further comprising test bench generating means for generating a random test vector with a separated simulation time repetitively input to an input key point of each of the modularized circuit portions, for utilizing the event-driven simulation.

9. A design verification device according to claim 6, further comprising:

a function of inputting expectation values relating to the circuit descriptions before and after the alteration in the verification means by simulation; and

comparing and determining means for comparing actual results of simulation from the verification means by simulation with the expectation values.

10. A design verification device according to claim 7, further comprising test bench generating means for generating a random test vector with a separated simulation time repetitively input to an input key point of each of the modularized circuit portions, for utilizing the event-driven simulation.

11. A design verification device according to claim 7, further comprising:

a function of inputting expectation values relating to the circuit descriptions before and after the alteration in the verification means by simulation; and

comparing and determining means for comparing actual results of simulation from the verification means by simulation with the expectation values.

12. A design verification device according to claim 8, further comprising:

a function of inputting expectation values relating to the circuit descriptions before and after the alteration in the verification means by simulation; and

comparing and determining means for comparing actual results of simulation from the verification means by simulation with the expectation values.

13. A design verification device according to claim 9, wherein the comparing and determining means compares a test vector for which a disagreement has occurred and an output according to the circuit descriptions before and after the alteration using this test vector with the expectation values, based on the actual results of simulation from the verification means by simulation, thereby to determine whether an alteration according to the expectation has been made or not.

14. A design verification device according to claim 9, wherein the expectation values are prepared by specifying an altered portion of a circuit before and after the alteration in the circuit description stage of a register transfer level, thereby to analyze the circuit description thereof, and by obtaining a test vector for which results of execution are different between before and after the alteration as well as results of the execution thereof, or by inputting a test vector and results of the execution thereof from a wave form indicated by a graphical user interface.

15. A design verification device according to claim 9, further comprising a function of registering as new expectation values an output of the circuit portion relating to the circuit descriptions before and after the alteration using the test vector for which the disagreed portion has occurred, thereby to make it possible to continue the event-driven simulation.

16. A design verification method for a semiconductor integrated circuit, the method comprising:

a process of inputting a circuit description before an alteration and a circuit description after the alteration,

a process of identifying an altered portion according to a disagreed portion;

a process of determining portions of the circuit description, which correspond to an output of each of registers, an external input to the circuit description and an output from the circuit description, as key points;

a process of cutting out a logic connected between each of the key points and a preceding key point, as a logic circuit group;

a process of carrying out formal verification for the logic circuit group that can assure an agreement or equivalence of the key point in the circuit descriptions before and after the alteration; and

a process of carrying out verification by utilizing an event-driven simulation for the logic circuit group that cannot assure an agreement or equivalence of the key point.

17. A design verification method according to claim 16, further comprising:

a process of inputting expectation values relating to the circuit descriptions before and after the alteration in the process of verification by simulation; and

a comparing and determining process of comparing actual results of simulation in the process of verification by simulation with the expectation values.

18. A design verification method according to claim 17, further comprising:

a process of registering as new expectation values an output of a circuit portion relating to the circuit descriptions before and after the alteration using the test vector for which a disagreement has occurred in the process of verification by simulation, thereby to make it possible to continue the event-driven simulation.

19. A design verification method for a semiconductor integrated circuit, the method comprising:

a process for inputting a circuit description before an alteration and a circuit description after the alteration;

a process of determining portions of the circuit description, which correspond to an output of each of registers, an external input to the circuit description and an output from the circuit description, as key points;

a process of cutting out a logic connected between each of the key points and a preceding key point, as a logic circuit group;

a process for identifying an altered portion for mapping the key point in the circuit descriptions, setting as an external input and output a key point at a closest position of which description before the alteration agrees with the description after the alteration from a portion of disagreement between the descriptions before and after the alteration, and modularizing a circuit portion including the altered portion;

a verification process by simulation for verifying the modularized circuit portion in the circuit descriptions before and alter the alteration respectively by utilizing an event-driven simulation; and

a formal verification process for verifying the logic circuit group except for the modularized circuit by utilizing formal verification for the circuit descriptions before and after the alteration respectively by reflecting only a node that has been regarded as the external input and output.

20. A design verification method according to claim 19, further comprising:

a process for identifying a logically altered portion, for assuming that there is a logically altered portion in the circuit descriptions before and after the alteration, when a logical disagreement occurred, and for regarding as external input and output the input to and output from a logic cone including a node that has been regarded as the external input and output and the logically altered portion out of logic cones following the formal verification, and thereby cutting out and modularizing the circuit description including the logically altered; and

a process for carrying out verification by simulation, for each modularized circuit portion in the circuit descriptions before and after the alteration.

21. A design verification method according to claim 19, further comprising:

a process of inputting expectation values relating to the circuit descriptions before and after the alteration in the process of verification by simulation; and

a comparing and determining process actual results of simulation in the process of verification by simulation with the expectation values.

22. A design verification method according to claim 20, further comprising:

a process of inputting expectation values relating to the circuit descriptions before and after the alteration in the process of verification by simulation; and

a comparing and determining process actual results of simulation in the process of verification by simulation with the expectation values.

23. A design verification method according to claim 21, further comprising a process of registering as new expectation values an output of a circuit portion relating to the circuit descriptions before and after the alteration using the test vector for which a disagreement has occurred in the process of verification by simulation, thereby to make it possible to continue the event-driven simulation.

24. A memory medium, readable by computer, for storing at least a design verification program for a semiconductor integrated circuit for operating a computer, the program comprising:

a process for inputting a circuit description before an alteration and a circuit description after the alteration,

a process of determining portions of the circuit description which correspond to an output of each of registers, an external input to the circuit description and an output from the circuit description, as key points;

a process of cutting out a logic connected between each of the key points and a preceding key point, as a logic circuit group;

a process for identifying an altered portion for mapping the key point in the circuit descriptions, setting as an external input and output a key point of which descriptions before and after the alteration agree with each other, said key point being closest to a disagreed portion between the descriptions before and after the alteration, and modularizing a circuit portion including the altered portion,

a verification process by simulation for verifying the modularized circuit portion in the circuit descriptions before and after the alteration respectively by utilizing an event-driven simulation; and

a formal verification process for verifying the logic circuit group except for the modularized circuit by utilizing formal verification for the circuit descriptions before and after the alteration respectively by reflecting only a node that has been regarded as the external input and output.

25. A memory medium according to claim 24, further comprising:

a process for identifying a logically altered portion, for assuming that there is a logically altered portion in the circuit descriptions before and after the alteration, when a logical disagreement occurred in the formal verification process, and for regarding as external input and output the input to and output from a logic cone including a node that has been regarded as the external input and output and the logically altered portion out of logic cones following the formal verification, and thereby cutting out and modularizing the circuit description including the logically altered; and

a process for carrying out verification by simulation, for each modularized circuit portion in the circuit descriptions before and after the alteration.

26. A memory medium according to claim 24, further comprising:

a process of inputting expectation values relating to the circuit descriptions before and after the alteration in the process of verification by simulation; and

a comparing and determining process actual results of simulation in the process of verification by simulation with the expectation values.

27. A memory medium according to claim 26, further comprising a process of registering as new expectation values an output of a circuit portion relating to the circuit descriptions before and after the alteration using the test vector for which a disagreement has occurred in the process of verification by simulation, thereby to make it possible to continue the event driven simulation.