Data processing: structural design – modeling – simulation – and em – Simulating electronic device or electrical system – Software program
Reexamination Certificate
1999-05-11
2003-11-25
Broda, Samuel (Department: 2123)
Data processing: structural design, modeling, simulation, and em
Simulating electronic device or electrical system
Software program
C703S014000, C716S030000
Reexamination Certificate
active
06654715
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Field of the Invention
The present invention relates to an apparatus and method for verifying a logical device for use in verifying all units which can be modelled as a finite state machine, for example, a sequential circuit and a protocol.
2. Description of the Related Art
A model check is well known as a method for verifying whether or not the design of a sequential circuit and a protocol satisfies the properties required for them. This method mathematically proves that a finite state machine satisfies or does not satisfy the property represented by a temporal logic.
A general form of a finite state machine can be represented by M=(Q, &Sgr;, &PHgr;, &dgr;, &lgr;, I).
Each of the symbols has the following meaning.
Q: set of states (finite)
&Sgr;: input alphabet (finite)
&PHgr;: output alphabet (finite)
&dgr;: transition relation function
&lgr;: output relation function
I: initial set of states
The transition relation function is a function set to 1 if the current state can be transient to the next state when the current state, the next state, and an input are entered, and otherwise set to 0. Although the transition relation function is a function for determining the next state, it is also able to represent a nondeterministic transition in which the next state cannot be uniquely determined by a current state and an input. When the transition is deterministic, the state transition can be represented as a function for obtaining the next state by the current state and an input. The above described output relation function similarly corresponds to the case where an output is nondeterministic.
Basically, all sequential circuits can be modelled as finite state machines. Therefore, when a logical device is designed, the finite state machine is popularly used as specification. For example, in synthesizing a logic, specification of a device is described by design description language. The description is converted by a synthesizing system to a finite state machine. Then, a state is realized by a flip-flop circuit or a register, and a transition relation function
6
and an output relation function &lgr; are realized by a combinational circuit.
The basic theory of the above described finite state machine is described in detail in chapter 2 of the reference document 1. In verifying a logical device, it is checked whether the operation of the logical device in the time sequence satisfies a required property. An applicable technology to attain the verification can be logical simulation and a model check.
The above described logical simulation is a process of simulating an operation by applying an appropriate input to a model of a device (description in design description language, gate level circuit chart, etc.). It is confirmed that an obtained operation satisfies the property.
A model check refers to an approach in which a logical device is modelled as a finite state machine or a network of a plurality of finite state machines, and it is mathematically determined whether or not the model satisfies the property. The model check is described in detail in the special articles (reference documents 2, 3, 4, 5, and 6 described later) in the Information Processing in September in 1994.
At present, the most practical model checking method is a symbol model checking method (refer to the reference documents 7 and 8 described later). In the symbol model checking method, the operation of the finite state machine is represented by a logical expression, and the verification procedure is realized by a logical function process. At this time, a logical function is represented by a binary decision diagram (BDD) (refer to the reference documents 9, 10, 11, 12, and 13 described later). To operate a finite state machine having an enormous number of states, an implicit expressing method using a logical function and an efficient logical function process using BDD are indispensable.
FIG. 1
shows the conventional technology, that is, an example of the finite state machine. In the above described model checking method, the symbol model checking method represents a logical device model of the Kripke structure using a logical function, checks whether or not a non-empty set of states which satisfies the specification represented by a computation tree logic exists.
The Kripke structure is a kind of nondeterministic finite automaton represented by the following equation using the finite set S of states, the transition relation R of states, the set Si of an initial state point, and the set L of a source proposition which is true in each state.
K
=(
S, R, Si, L
)
The computation tree logic is a kind of a temporal logic, and is represented by an operator A indicating ‘universal’, an operator E indicating ‘existential’, a temporal operator F indicating ‘future’, a temporal operator G indicating ‘global’, a temporal operator X indicating ‘next’, and a temporal operator U indicating ‘until’in addition to a common logic operator.
For example, the temporal operator AGa indicates that the logical expression a exists in the set of states reachable from the initial state. In this case, in a model of a logical device, all paths reachable from the initial state are traced, and it is checked whether or not all the paths can reach the state in which the logical expression a exists.
That is, the verifying operation in the symbol model checking method is an operation of tracing the state transition of the Kripke structure and confirming whether or not the computation tree logic indicating the specification exists in each state. This operation performs a set reduction operation for obtaining the smallest fixed point or the largest fixed point in a model according to a computation tree logic expression.
The above described set operation can be realized by combining an image computation Image ({q}) for obtaining a set of states reachable from a state set {q} in one state transition process with an inverse image computation Imagerev ({q}) for obtaining a set states reachable to a state set {q} in one state transition process.
For example, in the example of the finite state machine represented by a state transition between nine states q
0
through q
8
as shown in
FIG. 1
, examples of results of the image computation and the inverse image computation are represented by the following equations.
Image ({
q
0
})={
q
0
,
q
1
,
q
2
,
q
3
}
Image ({
q
0
,
q
2
})={
q
0
,
q
1
,
q
2
,
q
3
,
q
5
}
Imagerev ({
q
0
})={
q
0
,
q
1
}
Imagerev ({
q
5
})={
q
1
,
q
2
,
q
3
,
q
4
}
In the finite state machine shown in
FIG. 1
, when the temporal logic AFp using the logical expression p indicating the state q
8
is verified, the image computation is sequentially repeated from the initial state q
0
, and it is checked whether or not all paths transient from the initial state can actually reach the state q
8
. When the temporal logic EFp is verified, the inverse image computation is repeated from the state q
8
, and it is checked whether or not there is a path reaching the initial state q
8
.
In a common actual symbol model checking method, a set operation is replaced with a logical function process, and the logical function process becomes more efficient by representing the logical function by a binary decision diagram (BDD).
REFERENCE DOCUMENTS
1. J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Publishing Company, 1979.
2. Hiromi Hiraishi and Seiji Hamaguchi, ‘Formal Verifying Method based on Logical Function Process’, Information Process, vol. 35, No. 8, pp. 710-718, 1994.
3. Masahiro Fujita, Masami Yamazaki et al., ‘Application of Practical Design in Formal Verifying Method’, Information Process, vol. 35, No. 8, pp. 719-725, 1994.
4. Shinji Kimura, ‘Formal Timing Verification’, Information Process, vol. 35. No. 8, pp. 726-735, 1994.
5. Atsushi Takahara, ‘Formal Verification using Process Alge
Broda Samuel
Fujitsu Limited
Phan Thai
Staas & Halsey , LLP
LandOfFree
Apparatus, method, and storage medium for verifying logical... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Apparatus, method, and storage medium for verifying logical..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Apparatus, method, and storage medium for verifying logical... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3171462