VERIFICATION APPARATUS AND VERIFICATION METHOD

• US 20090019406A1
• Filed: 06/27/2008
• Published: 01/15/2009
• Est. Priority Date: 06/28/2007
• Status: Active Grant

• Current Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Original Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Inventors: Kawakatsu, Noritaka, Kawata, Hideji, Imai, Takeo, Endoh, Yusuke
• Granted Patent: US 8,578,308 B2
• Time in Patent Office: Days
• 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 can describe using function calls, the apparatus comprising:

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

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 statement to the variable; and

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

2. The apparatus according to claim 1, wherein the value assignment device includes:

an insertion device configured to insert a description that assigns the value corresponding to the meaning of the statement to the variable in the circuit description; and

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

3. The apparatus according to claim 2, wherein the description is inserted at a position of an instruction generated by the event in the circuit description.

4. The apparatus according to claim 1, further comprising a conversion device configured to convert the statement into a formula that expresses the condition using the variable.

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

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

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

8. The apparatus according to claim 1, which further comprises a simulation device configured to simulate the circuit description, and to output a signal change log which represents a change in value of the variable, and

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

9. 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.

10. 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 can describe using function calls, comprising:

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

detecting generation of the event at an arbitrary time on the continuous time series;

assigning a value corresponding to a meaning of the statement to the variable; and

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

11. The method according to claim 10, wherein the assigning includes:

inserting a description that assigns the value corresponding to the meaning of the statement to the variable in the circuit description; and

initializing the value of the variable immediately after determination of the condition.

12. The method according to claim 11, wherein the description is inserted at a position of an instruction generated by the event in the circuit description.

13. The method according to claim 10, further comprising converting the statement into a formula that expresses the condition using the variable.

14. The method according to claim 10, wherein the statement includes a statement which designates start of the function call.

15. The method according to claim 10, wherein the statement includes a statement which designates end of the function call.

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

17. The method according to claim 10, further comprising simulating the circuit description,

outputting a signal change log which represents a change in value of the variable, and

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

18. The method according to claim 10, 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.

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

20. A 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 can describe using function calls, which when executed by a computer results in performance of steps comprising:

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

detecting generation of the event at an arbitrary time on the continuous time series, and assigning a value corresponding to a meaning of the statement to the variable; and

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