Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1998-10-13
2001-06-12
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
Reexamination Certificate
active
06247163
ABSTRACT:
BACKGROUND
1. Field of the Invention
This invention pertains generally to digital circuit design and particularly to combinational equivalence verification.
2. Background of the Invention
Today's logic circuits are so complex that circuit designers must use computer-based techniques to help them in their task. Some of these techniques transform a specification of a circuit into an equivalent implementation of the circuit. During this transformation, errors may be introduced into the implementation. Accordingly, checking must be performed to verify that the implementation conforms with the specification. Combinational equivalence checking is one form of checking.
When applied to a pair of sequential circuits, combinational equivalence checking typically consists of two steps: latch mapping and verification. The first step constructs a latch mapping (also known as a register mapping) by identifying corresponding latches in the two designs to be compared. Then, it is possible to break the circuits into corresponding combinational blocks (e.g., single-output, multiple-input Boolean functional blocks). The second step is to verify whether the corresponding combinational blocks are equivalent. If the corresponding blocks are equivalent, the circuits are functionally equivalent.
There has been much research on the second step, verification. For example, A. Kuehlmann and F. Krohm, “Equivalence Checking Using Cuts and Heaps,” DAC, 1997, and D. K. Pradhan, D. Paul, and M. Chatterjee, “VERILAT: Verification Using Logic Augmentation and Transformations,” ICCAD, 1996, are recent examples. However, there has been little research on the first step, constructing a latch mapping.
Existing commercial tools for constructing a latch mapping use heuristics based on signal names or circuit structure. However, tools that perform design transformations such as synthesis or clock tree insertion often do not preserve signal names, especially when a design is flattened as part of the transformation. If two combinational blocks are found to be inequivalent, it may be because of an incorrect latch mapping rather than a bug in the circuit. This possible error in the latch mapping complicates debugging.
Accordingly, there is a need for a method and system for constructing a latch mapping that accurately maps corresponding latches in the two circuit designs. Preferably, the method and system should not use heuristics based on signal names or circuit structure to construct the latch mapping.
SUMMARY OF THE INVENTION
The above needs are met by a method and system for performing latch mapping for combinational equivalence checking that is not based on signal names. The method and system start with two circuits: an implementation and a specification. The state holding elements of each circuit are referred to as “latches.” The latches are represented as L, the states are represented as S, and a transition function &dgr; is defined. Given an input vector I and a state S, the transition function &dgr; produces the next state. In addition, a predicate P is defined to be semi-inductive if ∀S ∀I [P(S)
P(&dgr;(S,I))]. Latch mappings are represented with a predicate M such that latches l
1
and l
2
are mapped together if and only if M(l
1
, l
2
) is true.
The method and system construct an initial mapping that, in one embodiment, maps every latch to every other latch. This mapping is then iteratively refined until it is semi-inductive. The refinement is performed by randomly producing a state that satisfies the mapping. Then, a random input vector is applied to the circuits and the resulting state is determined. If the resulting state does not satisfy the mapping, then a new mapping is constructed reflecting the resulting state. This new mapping is a refinement of the previous mapping.
If the resulting state after the random input vector is applied satisfies the mapping, then, for each pair of latches mapped together, combinational equivalence checking is used to show whether the combinational blocks that drive the pair of latches are equivalent for all combined states that satisfy the mapping. If the blocks are not equivalent, the combinational equivalence checker will produce a counter-example including an input vector. The input vector is applied to the circuits and a new mapping is constructed reflecting the resulting state. If every pair of latches that is mapped together is examined without producing a counter-example, then the mapping is semi-inductive. This mapping is called M*.
Once M* is found, the next determination is whether it forces output equality. This determination is performed by using combinational equivalence checking on the combinational blocks driving the primary outputs of the implementation and specification.
If M* does not force output equality, then the two circuits are not combinationally equivalent. Accordingly, the present invention includes an interactive procedure for locating a bug in a combinational block of the implementation. The user determines whether the latches of the local inputs to the combinational blocks that drive the outputs in the implementation and the specification are properly mapped together. If the latches are properly mapped together, then there is a bug in a combinational block driving the output of the implementation. Otherwise, the user selects a mapping for the latches that are local inputs to the combinational blocks driving the previously selected latches. This process iterates until the combinational block having the bug is found.
If M* does force output equality, then the next determination is whether the implementation satisfies a supplied reset condition, if any. The implementation satisfies a reset condition if there are no implementation latches mapped together in M*. If implementation latches are mapped in the same equivalence class, then the implementation can be guaranteed to conform with the specification only if the implementation latches mapped together are assumed to have the same value in the reset state.
In one embodiment, the method and system for performing latch mapping is expanded to cover ternary latch mappings having “don't care” conditions. When used with ternary latch mappings, the method and system define a pre-order, rather than an equivalence relation, between the latches. Conformance relationships are described with classes having links between them representing those classes having latches that are strictly less than the latches of another class. One embodiment determines conformance relationships by selecting a representative latch from each class and testing for conformance among the representative latches.
REFERENCES:
patent: 5638381 (1997-06-01), Cho et al.
patent: 6035109 (2000-03-01), Ashar
C. A. J. van Eijk;Sequential Equilvalence Checking Without State Space Transversal;1998 EDAA.
C. A. J. van Eijk;Formal Methods for the Verification of Digital Circuits;Sep. 1997.
Burch Jerry R.
Singhal Vigyan
Cadence Design Systems Inc.
Do Thuan
Lyon & Lyon LLP
Smith Matthew
LandOfFree
Method and system of latch mapping for combinational... 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 of latch mapping for combinational..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system of latch mapping for combinational... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2448145