Data processing: structural design – modeling – simulation – and em – Simulating electronic device or electrical system – Circuit simulation
Reexamination Certificate
1999-09-09
2004-06-15
Teska, Kevin J. (Department: 2123)
Data processing: structural design, modeling, simulation, and em
Simulating electronic device or electrical system
Circuit simulation
C703S015000, C703S002000, C716S030000
Reexamination Certificate
active
06751582
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Technical Field
The present invention relates to an improved method for verifying designs and, in particular, to a method of formal verification which provides the user with a simple method of extracting the desired data.
2. Description of Related Art
Designers and inventors have long sought methods of confirming their designs without actually building the design in physical form and using trial and error. With the advent of computers, simulation has become and still is the most common hardware verification framework in use today. Simulation requires that a battery of tests be run through a model of the implementation of a particular design, trying out a number of possible input variations, and then checking to see that the model meets the specifications. Simulation consists of the application of an ordered sequence of input vectors to a particular model that is being tested.
Simulation is polynomial in complexity with respect to the model being tested. However, for complex designs, the amount of behavioral coverage obtainable through simulation decreases rapidly. As designs become more complex, simulation becomes very inefficient in verifying the design. Hence, simulation cannot be done exhaustively even for moderately large designs.
Recently, there has been increased interest in formal verification methods. In formal verification methods, mathematical reasoning frameworks are implemented which exhaustively cover the design behavior. The method consists of using formal proofs to verify that a design satisfies certain properties, which are sometimes referred to as formal specifications.
While the algorithms used in formal verification methods tend to be exponential in complexity with respect to the design size, the results in the hands of skilled users have proven its utility. Symbolic model checking is a type of formal verification and is now a common part of the design validation process. Model checking is a fully automated technique which verifies that a set of properties specified with temporal formulas will hold for a given design.
Referring now to
FIG. 1
, algorithm
100
for such a technique requires a formal description of design environment
120
. That is, a definition of the conditions to which the design under test is to be subjected must be provided to the algorithm. The algorithm also requires a description of the hardware itself, called the model
110
, and a property
130
that is to be verified by algorithm
135
. Once environment
120
, model
110
, and property
130
are input, a determination is made by algorithm
135
as to whether property
130
passes or fails at block
140
.
In addition to a “pass or fail” result, a cycle-by-cycle trace of all signal values illustrating a counter-example is typically provided at block
150
upon a failure. A counter-example is a stream of execution which violates the specified property. Also, a trace illustrating a witness is typically provided at block
160
upon a pass. A witness is a stream of execution which non-trivially satisfies the specified property.
For example, if the property is “if REQ is active, then GNT must be active in 3 cycles,” a nontrivial stream of execution which satisfies this property is one which shows that the request REQ becomes active. If so, then the grant GNT will be checked in three cycles, and if it is not active, then the property will fail. An example of a stream of execution which trivially satisfies the property is the case in which REQ never occurs. Thus, there will be no opportunity for the property to fail, and hence no meaningful trace to display.
In order to generate these traces, the model checker arbitrarily calculates a set of valuations of the state variables in the model which comprise only one possible witness or counter-example. If the user is happy with the trace that was generated by the model checker, then the model checking procedure is finished at block
170
. However, if the user is not satisfied with the trace that was generated, either model
110
or environment
120
is modified in order to get a more satisfactory trace for property
130
.
The complexity of model checking is also exponential in relation to the size of the model, the environment, and the property to be tested. The reason for this is that the modeling technique or tool performs a breadth-first exhaustive reachability calculation. That is, beginning with all initial states, all states reachable in one “simulation step”(denoted Image
1
) are explored. Then, all states reachable in two simulation steps (denoted Image
2
) are explored, and so on until no new states are found. One reason that breadth-first algorithms are typically used rather than depth-first algorithms is to avoid excessively long traces if the error could manifest itself in a shorter period of time using a breadth-first algorithm.
One shortcoming of formal verification techniques is the “state-space explosion.” This problem is seen as the number of state variables in a model is increased. The number of states in a model with N state variables may equal 2
N
. Thus, as the number of state variables is increased, the complexity of the model increases exponentially. Therefore, such a formal verification method has limited application in industrial designs because of the complexity that usually exists in industrial designs.
Model checkers typically support the notion of the “invariant” or “invar” keyword, whose arguments are a set of Boolean properties. For example, using the command “invar p” truncates the state space exploration of the tool to only consider those states where “p” is true. All encountered states where p is not true are discarded along with their successors, generally. (Note that some of the successors will not be discarded if they are encountered along a different path where “p” is always true.) Because certain states and paths are ignored due to the invariants, the complexity of the model checking run is thereby reduced.
Imposing cycle-specific restrictions using traditional model checking tools requires the user to manually generate an automaton to count cycles and create standard invariants of the form “invar (automata=1)→(REQ=1)”, “invar (automata=2)→(GNT=0)”, etc. The use of an automaton in this manner creates additional state variables causing even more of a state-space explosion. The additional complexity of the extra automaton may outweigh the benefit of the use of such invariants. The verification tool in many cases consumes more CPU time/memory than in the original run where the automaton was not used. This manual and computational complexity is suffered merely to generate one tailored trace.
An automaton is a finite state machine (FSM). It is a state transition system that consists of a set of states, and a set of transitions defined from one state to the next. For example, consider the array <S, I, T> where S is the set of states, I is the set of inputs to the automaton, and T is the transition function. Intuitively, a Finite State Machine (FSM) or an automaton starts in an “initial state.” From its present state, under control of the present input, T defines the next state to which the automaton will transition.
As noted earlier, formal verification (such as model checking) is roughly exponential in relation to the size of the model. Using the prior art, if a trace is obtained which is undesirable, the designer typically couples onto the model under test an automaton which does nothing more than count cycles. A set of user-defined cycle-specific invariants (as above) are then introduced to guide the state space search. This automaton initializes to count=0. Each transition increments its value by one. The implication is that with the automaton added, model checking becomes exponential in relation to the size of the model PLUS the size of the automaton. While the invariants prune the state space search, the constrained run is typically even more costly than the original unconstrained run due to the extra automaton.
Furthermore,
Andersen Flemming
Baumgartner Jason Raymond
Roberts Steven Leonard
Carwell Robert M.
Teska Kevin J.
Thangavelu Kandasamy
Yee Duke W.
Yociss Lisa L. B.
LandOfFree
Method and system for enhanced design validation through... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method and system for enhanced design validation through..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for enhanced design validation through... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3362764