Design verification system and method

• US 20020038203A1
• Filed: 09/25/2001
• Published: 03/28/2002
• Est. Priority Date: 09/25/2000
• Status: Active Grant

• Current Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Original Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Inventors: Tsuchiya, Takehiko
• Granted Patent: US 7,263,478 B2
• Time in Patent Office: Days
• US Class Current: 703/15
• CPC Class Codes: G06F 30/33 Design verification, e.g. functional simulation or model checking

Abstract

A system for verifying a circuit represented with a circuit description including a plurality of descriptions, the system comprising a simulator configured to carry out a logic simulation of the circuit description with the use of a test bench for the circuit description, an extractor configured to extract descriptions unexecuted in the logic simulation according to code coverage information for the circuit description, an examiner configured to examine whether or not there is a possibility of executing the extracted unexecuted descriptions, and a prohibited-input-checker generator configured to generate an test pattern to execute the unexecuted description that there is a possibility of executing, and to generate a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to an input pattern of the test pattern to execute the unexecuted description if the test bench is regard as a prohibited input under a specification at a logic simulation using the test pattern to execute the unexecuted description.

Claims

1. A system for verifying a circuit represented with a circuit description including a plurality of descriptions, the system comprising:

a simulator configured to carry out a logic simulation of the circuit description with the use of a test bench for the circuit description;

an extractor configured to extract descriptions unexecuted in the logic simulation according to code coverage information for the circuit description;

an examiner configured to examine whether or not there is a possibility of executing the extracted unexecuted descriptions; and

a prohibited-input-checker generator configured to generate a test pattern to execute the unexecuted description that there is a possibility of executing, and to generate a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to an input pattern of the test pattern to execute the unexecuted description if the test bench is regard as a prohibited input under a specification at a logic simulation using the test pattern to execute the unexecuted description.

2. The system as claimed in claim 1, wherein:

the examiner employs a model checking technique when examining whether or not there is a possibility of executing the extracted unexecuted descriptions.

3. A system for verifying a circuit represented with a circuit description including a plurality of descriptions, the system comprising:

a simulator configured to carry out a logic simulation of the circuit description with the use of a test bench for the circuit description;

an extractor configured to extract descriptions unexecuted in the logic simulation according to code coverage information for the circuit description;

an examiner configured to examine whether or not there is a possibility of executing the extracted unexecuted descriptions; and

an unexecuted-description-checker generator configured to generate an unexecuted-description checker to inform that one of the descriptions which is unable to generate a test bench is going to be executed in a logic simulation.

4. The system as claimed in claim 3, further comprising:

the prohibited-input-checker generator configured to generate a test pattern to execute the unexecuted description that there is a possibility of executing, and to generate a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to an input pattern of the test pattern to execute the unexecuted description if the test bench is regard as a prohibited input under a specification at a logic simulation using the test pattern to execute the unexecuted description.

5. The system as claimed in claim 3, wherein:

the examiner employs a model checking technique when examining whether or not there is a possibility of executing the extracted unexecuted descriptions.

6. A method of verifying a circuit represented with a circuit description including a plurality of descriptions, the system comprising:

carrying out a logic simulation of the description having a possibility of being executed, with the use of a test bench for the circuit description;

extracting descriptions unexecuted in the logic simulation according to code coverage information for the circuit description;

examining whether or not there is a possibility of executing the extracted unexecuted descriptions;

generating a test pattern to execute the unexecuted description that there is a possibility of executing; and

if the test bench is regard as a prohibited input under a specification at a logic simulation using the test pattern to execute the unexecuted description, generating a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to an input pattern of the test pattern to execute the unexecuted description.

7. The method as claimed in claim 6, wherein:

examining whether or not there is a possibility of executing the extracted unexecuted descriptions employs a model checking technique.

8. A method of verifying a circuit represented with a circuit description including descriptions, the method comprising:

carrying out a logic simulation of the circuit description with the use of a test bench for the circuit description;

extracting descriptions unexecuted in the logic simulation according to code coverage information for the circuit description;

examining whether or not there is a possibility of executing the extracted unexecuted descriptions; and

generating an unexecuted-description checker to inform that one of the descriptions which is unable to generate a test bench is going to be executed in a logic simulation.

9. The method as claimed in claim 8, further comprising, after examining whether or not there is a possibility of executing the extracted unexecuted descriptions:

generating a test pattern to execute the unexecuted description that there is a possibility of executing, and to generate a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to an input pattern of the test pattern to execute the unexecuted description if the test bench is regard as a prohibited input under a specification at a logic simulation using the test pattern to execute the unexecuted description.

10. The method as claimed in claim 8, wherein:

examining whether or not there is a possibility of executing the extracted unexecuted descriptions employs a model checking technique.

11. The method as claimed in claim 8, further comprising:

if it is determined that there is no possibility of executing the extracted unexecuted descriptions, excluding the unexecuted descriptions from data to calculate code coverage information.

13. The method as claimed in claim 12, further comprising:

if it is determined that the result satisfies the specifications, then;

picking up an input pattern at the boundary of each subordinate system; and

adding the picked-up input pattern to a database to store test benches for the subordinate systems.

14. The method as claimed in claim 12, further comprising:

if it is determined that the unexecuted descriptions have not been executed in the logic simulation of the superordinate system, determining whether or not new branches and paths are generated by combining the subordinate systems into the superordinate system; and

if it is determined that new branches or paths are generated by combining the subordinate systems, generating input checkers and unexecuted-description checkers for the superordinate system.

16. The product as claimed in claim 15, wherein:

examining whether or not there is a possibility of executing the extracted unexecuted descriptions employs a model checking technique.

18. The product as claimed in claim 17, further comprising, after examining whether or not there is a possibility of executing the extracted unexecuted descriptions:

generating an test pattern to execute the unexecuted description that there is a possibility of executing, and to generate a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to an input pattern of the test pattern to execute the unexecuted description if the test bench is regard as a prohibited input under a specification at a logic simulation using the test pattern to execute the unexecuted description.

19. The product as claimed in claim 17, wherein:

examining whether or not there is a possibility of executing the extracted unexecuted descriptions employs a model checking technique.

20. The product as claimed in claim 17, further comprising:

if it is determined that there is no possibility of executing the extracted unexecuted descriptions, excluding the unexecuted descriptions from data to calculate code coverage information.

12. A method of verifying a superordinate system containing at least two subordinate systems, the method comprising:

determining whether or not a test bench to carry out a logic simulation of the superordinate system includes a prohibited input pattern of at least one of the subordinate systems;

if it is determined that the superordinate system includes no prohibited input pattern of the subordinate systems, executing a logic simulation with the use of the test bench;

determining whether or not descriptions unexecuted in logic simulations of the subordinate systems have been executed in the logic simulation of the superordinate system;

if it is determined that the unexecuted descriptions have been executed in the logic simulation of the superordinate system, determining whether or not a result of the logic simulation of the superordinate system related to the unexecuted descriptions satisfies specifications;

if it is determined that the result shows a violation of the specifications and if the cause of the violation is a prohibited input pattern, generating a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to the prohibited input pattern; and

eliminating the unexecuted descriptions from an unexecuted-description checker database to store unexecuted descriptions.

15. A computer program product including computer usable media having computable readable code embodied therein executing a method for verifying a circuit represented with a circuit description including a plurality of descriptions, the method comprising:

carrying out a logic simulation of the description having a possibility of being executed, with the use of a test bench for the circuit description;

extracting descriptions unexecuted in the logic simulation according to code coverage information for the circuit description;

examining whether or not there is a possibility of executing the extracted unexecuted descriptions;

generating an test pattern to execute the unexecuted description that there is a possibility of executing; and

if the test bench is regard as a prohibited input under a specification at a logic simulation using the test pattern to execute the unexecuted description, generating a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to an input pattern of the test pattern to execute the unexecuted description.

17. A computer program product including computer usable media having computable readable code embodied therein executing a method for verifying a circuit represented with a circuit description including descriptions, the method comprising:

carrying out a logic simulation of the circuit description with the use of a test bench for the circuit description;

extracting descriptions unexecuted in the logic simulation according to code coverage information for the circuit description;

examining whether or not there is a possibility of executing the extracted unexecuted descriptions; and

generating an unexecuted-description checker to inform that one of the descriptions which is unable to generate a test bench is going to be executed in a logic simulation.

21. A computer program product including computer usable media having computable readable code embodied therein executing a method for verifying a superordinate system containing at least two subordinate systems, the method comprising:

determining whether or not a test bench to carry out a logic simulation of the superordinate system includes a prohibited input pattern of at least one of the subordinate systems;

if it is determined that the superordinate system includes no prohibited input pattern of the subordinate systems, executing a logic simulation with the use of the test bench;

determining whether or not descriptions unexecuted in logic simulations of the subordinate systems have been executed in the logic simulation of the superordinate system;

if it is determined that the unexecuted descriptions have been executed in the logic simulation of the superordinate system, determining whether or not a result of the logic simulation of the superordinate system related to the unexecuted descriptions satisfies specifications;

if it is determined that the result shows a violation of the specifications and if the cause of the violation is a prohibited input pattern, generating a prohibited-input checker to check whether or not an input pattern of a logic simulation to be carried out is equal to the prohibited input pattern; and

eliminating the unexecuted descriptions from an unexecuted-description checker database to store unexecuted descriptions.

22. The product as claimed in claim 21, further comprising:

if it is determined that the result satisfies the specifications, then;

picking up an input pattern at the boundary of each subordinate system; and

adding the picked-up input pattern to a database to store test benches for the subordinate systems.

23. The product as claimed in claim 21, further comprising:

if it is determined that the unexecuted descriptions have not been executed in the logic simulation of the superordinate system, determining whether or not new branches and paths are generated by combining the subordinate systems into the superordinate system; and

if it is determined that new branches or paths are generated by combining the subordinate systems, generating input checkers and unexecuted-description checkers for the superordinate system.