Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1998-07-29
2001-02-20
Teska, Kevin J. (Department: 2123)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C703S014000, C714S724000
Reexamination Certificate
active
06192505
ABSTRACT:
FIELD OF THE INVENTION
This invention relates in general to model checking and, in particular, to model reduction techniques prior to computer-implemented model checking.
BACKGROUND OF THE INVENTION
When designing integrated circuits including combinatorial and sequential gates and circuit elements, tools are used to check the integrity of the final design before proceeding to mass-production. The tools are computer programs which require as input a mathematical model of the integrated circuit design and a specification of desired design criteria. Thus, for example, a Flip-Flop circuit element may generate an acknowledge signal (ACK) responsive to a request signal (REQ) and the design specification may require that the REQ signal produces the ACK signal within three clock cycles.
From knowledge of the design specification and the mathematical model of the integrated circuit, the computer determines whether the model meets the specified design criteria. Such a program solves a state machine having a large number of variables dependent, of course, on the model complexity. Thus, the more gates and memory elements in the integrated circuit, the more complex is the model and the greater the number of variables in the state machine to be solved. In practice, the more complex the design the greater is the size of memory which the computer requires to solve the state machine; and the longer the calculation time. There exists, therefore, a need to reduce the model complexity without compromising on the integrity of the model checking.
Prior art techniques relate principally to manual and/or trivial reduction of the number of state variables by eliminating obviously redundant circuit elements. For example,
FIG. 1
shows part of a logic circuit depicted generally as
10
comprising an AND-gate
11
whose output is fed to the REQ input of a Flip-Flop
12
having an ACK output
13
and a CLK input
14
. A first input
15
of the AND-gate
11
is driven by the output of a sub-circuit designated
16
which may itself include a large number of logic elements. A second input
17
of the AND-gate
11
is tied to logic “0”.
In such an arrangement, the output of the AND-gate
11
will always be logic “0” regardless of any changes that occur in the logic state of the first input
15
of the AND-gate
11
consequent to operation of the sub-circuit
16
. In this trivial example, the AND-gate
11
as well as the Flip-Flop
12
may be replaced by a line of constant logic level “0” thereby reducing the number of state space variables in the mathematical model representative of the logic circuit
10
.
Another example of useful reduction is the elimination of signals that are not in the so-called “cone of influence” of the circuit being verified. Thus, if only part of the circuit is being verified, then any other parts whose behavior does not alter the part under verification can be eliminated. Thus, in the example shown in
FIG. 1
, suppose that only that part of the logic circuit
10
which is connected to the ACK output
13
of the Flip-Flop
12
is being verified. In such case, not only can the AND-gate
11
and the Flip-Flop
12
be replaced by a line of constant logic level “0”, but the sub-circuit
16
can be eliminated altogether. This follows since the sub-circuit
16
is not in the cone of logic being verified. This, of course, significantly reduces the complexity of the model being tested resulting in faster processing time and lower memory requirements.
However, it is not always convenient or possible to reduce the number of space state variables in such manner and even when manual reduction is feasible, it is only amenable to obvious or trivial reductions. Non-obvious reductions may still be possible and in this case conventional manual techniques do not succeed in optimal reduction. It would thus be desirable to offer a systematic approach to model reduction suitable for computer-implementation allowing non-obvious reductions to be achieved and thus achieving optimal reduction and maximum saving of computer resources.
SUMMARY OF THE INVENTION
This object is realized in accordance with the invention by means of a computer-implemented method for systematically eliminating redundant circuit elements in a state machine of a model having sequential circuit elements possessing one of a fixed number of possible states, said method comprising the steps of:
(a) sorting the sequential circuit elements into groups having an initial state which is determinate i.e. equal to a known one of said fixed number of possible states or which is indeterminate,
(b) storing the state of each circuit element whose state is determinate,
(c) for each circuit element whose state is determinate, calculating its next state,
(d) moving each circuit element in (c) whose next state is different to the state thereof stored in (b) to the group of indeterminate circuit elements,
(e) repeating steps (b) to (d) in respect of all remaining determinate circuit elements until no further circuit elements are moved in step (d),
(f) replacing each of the remaining determinate circuit elements by a constant equal to its corresponding state, and
(g) eliminating any circuit elements whose respective output is connected to one or more of the circuit elements replaced in (f) and to no other circuit elements.
Such a method is particularly applicable to the reduction of sequential circuit elements in a digital logic circuit having binary logic states “0” and “1” prior to design verification thereof. However, the method is equally applicable to state machines representative of non-binary circuits whose elements have one of a fixed number of possible states.
REFERENCES:
patent: 5566187 (1996-10-01), Abramovici et al.
patent: 5657240 (1997-08-01), Chakradhar et al.
patent: 5761487 (1998-06-01), Yuguchi
Cheng, “On Removing Redundancy in Sequential Circuits”, Proceedings of the 28 ACM/IEEE Design Automation Conference, pp. 164-169, 1991.
Ashar et al, “Irredundant Interacting Sequential Machines Via Optimal Logic Synthesis”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, pp. 311-325, 1991.
Baumgartner et al, “An Overview and Application of Model Reduction Techniques in Formal Verification”, IEEE International Performance, Computing, and Communications, pp. 165-171, Feb. 1998.
Dordick, “A Chip Verification On a Large Scale”, IBM Research Magazine, Issue 2, 1996, found at: http://www.research.ibm.com/resources/magazine/1996/issue_2/verify296.html.
Beer Ilan
Eisner Cindy
Rodeh Yoav
Broda Samuel
Browdy and Neimark
International Business Machines - Corporation
Teska Kevin J.
LandOfFree
Method and system for reducing state space variables prior... 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 reducing state space variables prior..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for reducing state space variables prior... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2605263