Verification apparatus and verification method

• US 8,578,308 B2
• Filed: 06/27/2008
• Issued: 11/05/2013
• Est. Priority Date: 06/28/2007
• Status: Expired due to Fees

• Current Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Original Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Inventors: Endoh, Yusuke, Imai, Takeo, Kawata, Hideji, Kawakatsu, Noritaka
• Primary Examiner(s): Rossoshek, Helen
• Application Number:
  US12/163,486
• Publication Number:
  US 20090019406A1
• Time in Patent Office: 1,957 Days
• Field of Search: 716/100, 716/102, 716/103, 716/106, 716/136, 703/2, 703/13, 703/14
• US Class Current: 716/106
• CPC Class Codes: G06F 30/33 Design verification, e.g. functional simulation or model checking
• CPC Class Codes: G06F 30/3308 using simulation
• CPC Class Codes: G06F 30/3312 Timing analysis
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A variable is allocated to a statement that designates an event associated with a function call in an assertion. Generation of the event at an arbitrary time on a continuous time series is detected, and a value corresponding to a meaning of the statement is assigned to the variable. Whether or not a condition corresponding to the meaning of the statement is satisfied is determined based on the value of the variable at each time on a discrete time series.

Claims

1. A verification apparatus, which verifies, at respective times on a discrete time series, a circuit description that describes a communication between circuit components, in which a signal value changes on a continuous time series, by a design description language that describes the communication as a function call, the apparatus comprising:

an allocation device configured to allocate a new variable to an extended statement that designates an event associated with the function call in an extended assertion described using a property description language;

a conversion device configured to convert the extended statement into a formula that expresses a condition using the new variable;

a value assignment device configured to detect generation of the event at an arbitrary time on the continuous time series, and to assign a value corresponding to a meaning of the extended statement to the new variable so that a description of variable assignment is inserted in the circuit description;

a simulation device configured to simulate the circuit description in which the description of variable assignment is inserted; and

a determination device configured to determine based on the value of the new variable at each time on the discrete time series if the condition corresponding to the meaning of the extended statement is satisfied.

2. The apparatus according to claim 1, further comprising

an initialization device configured to initialize the value of the new variable immediately after determination of the condition.

3. The apparatus according to claim 2, wherein the description of variable assignment is inserted at a position of an instruction that generates the event in the circuit description.

4. The apparatus according to claim 1, wherein the extended statement includes a statement which designates start of the function call.

5. The apparatus according to claim 1, wherein the extended statement includes a statement which designates end of the function call.

6. The apparatus according to claim 1, wherein the extended statement includes a statement which designates that the function call is in process.

7. The apparatus according to claim 1, wherein the simulation device outputs a signal change log which represents a change in value of the new variable, and

in which the condition is determined based on the signal change log.

8. The apparatus according to claim 1, wherein each time on the discrete time series is a verification unit time corresponding to a timing at which true or false of a logical formula expressed by the assertion is to be determined.

9. A verification method of verifying, at respective times on a discrete time series, a circuit description that describes a communication between circuit components, in which a signal value changes on a continuous time series, by a design description language that describes the communication as a function call, comprising:

allocating, at an allocation device, a new variable to an extended statement that designates an event associated with the function call in an extended assertion described using a property description language;

converting, at a conversion device, the extended statement into a formula that expresses a condition using the new variable;

detecting, at a value assigning device, generation of the event at an arbitrary time on the continuous time series;

assigning, at the value assigning device, a value corresponding to a meaning of the extended statement to the new variable so that a description of variable assignment is inserted in the circuit description;

simulating, at a simulation device, the circuit description in which the description of variable assignment is inserted; and

determining, at a determination device, based on the value of the new variable at each time on the discrete time series if the condition corresponding to the meaning of the extended statement is satisfied.

10. The method according to claim 9, further comprising:

initializing, at an initialization device, the value of the new variable immediately after determination of the condition.

11. The method according to claim 10, wherein the description of variable assignment is inserted at a position of an instruction that generates the event in the circuit description.

12. The method according to claim 9, wherein the extended statement includes a statement which designates start of the function call.

13. The method according to claim 9, wherein the extended statement includes a statement which designates end of the function call.

14. The method according to claim 9, wherein the extended statement includes a statement which designates that the function call is in process.

15. The method according to claim 9, wherein the simulating, at the simulation device comprises

outputting, at the simulation device, a signal change log which represents a change in value of the new variable, and

wherein the condition is determined based on the signal change log.

16. The method according to claim 9, wherein each time on the discrete time series is a verification unit time corresponding to a timing at which true or false of a logical formula expressed by the assertion is to be determined.

17. The method according to claim 16, wherein the verification unit time is a timing at which a clock of the circuit component goes high.

18. A non-transitory computer readable storage medium storing instructions of a computer program for verifying, at respective times on a discrete time series, a circuit description that describes a communication between circuit components, in which a signal value changes on a continuous time series, by a design description language that describes the communication as a function call, which when executed by a computer results in performance of steps comprising:

allocating a new variable to an extended statement that designates an event associated with the function call in an extended assertion described using a property description language;

converting the extended statement into a formula that expresses a condition using the new variable;

detecting generation of the event at an arbitrary time on the continuous time series, and assigning a value corresponding to a meaning of the extended statement to the new variable so that a description of variable assignment is inserted in the circuit description;

simulating the circuit description in which the description of variable assignment is inserted; and

determining based on the value of the new variable at each time on the discrete time series if the condition corresponding to the meaning of the extended statement is satisfied.