Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1999-10-25
2002-09-24
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
Reexamination Certificate
active
06457162
ABSTRACT:
FIELD OF THE INVENTION
The present invention relates generally to digital circuit design verification, and more particularly to formal verification across differing circuit architectures.
BACKGROUND OF THE INVENTION
In the design of digital integrated circuits, it is often desirable to be able to ascertain whether two circuits are equivalent. Equivalency of two combinational circuits can be defined, in a functional sense, as follows. A first design and a second design are equivalent if both accept the same set of input combinations, and if both produce the same output combination for each input combination.
The determination of circuit equivalency has become increasingly important with the emergence of large scale digital integrated circuits that incorporate an entire system on a chip. Such chips have reached a size and complexity level where it is difficult to verify them, in a timely manner, using traditional gate-level simulation. As a result, static verification tools are being more widely utilized by chip designers. Examples of such static-verification tools are PrimeTime, a static-timing analyzer, and Formality, a formal verification tool. Both PrimeTime and Formality are products of Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Static-timing analysis is used to analyze and verify the timing of the design and formal verification is used to verify a design's functionality by proving functional equivalence.
A design methodology that utilizes formal verification can reduce the number of time-consuming gate-level simulation runs. In a typical design process, utilizing logic synthesis and formal verification tools, the designer specifies his or her initial design at the register-transfer level (RTL). This RTL source specification is translated into a gate-level netlist by a logic synthesis tool, such as Design Compiler, produced by Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Formal verification is then used to compare the functional equivalency of the RTL source specification to the post-synthesis gate-level netlist. This gate-level netlist may then undergo several succeeding transformations that are intended to produce equivalent gate-level netlists. Such succeeding transformations can include: scan chain insertion, clock-tree synthesis, in-place optimization and manual editing. After each of these succeeding transformations, formal verification can be used to verify that the result of the latest transformation is functionally equivalent to the resulting gate-level netlist of the preceding transformation. For each of these comparisons a known-to-be-correct design (reference design) is compared against a design of unknown correctness (implementation design).
While formal equivalence checkers generally provide better coverage than gate-level simulation, such formal equivalency checking is fundamentally an NP-complete problem and therefore existing algorithms do not use reasonable memory or CPU resources for certain classes of circuits.
For example, (binary decision diagrams) BDDs have been successfully used for formal equivalency checking, but there are many functions for which the size of the BDD is exponential with respect to the size of the circuit being verified. This is most commonly known to occur with multiplier circuits. BDDs are generally incapable of verifying multipliers with more than sixteen bits in the multiplicands.
Other approaches to formal equivalency checking utilize the fact that (as discussed above) the implementation circuit is derived directly from the reference circuit through synthesis. Because of this, the two circuits usually have a great deal of structural similarity. Certain verification algorithms take advantage of this similarity by trying to find internal equivalence points and simple implications which enable the verification process to succeed. As long as the implementation circuit is directly synthesized from the reference circuit, such approaches can be successful and have been shown to verify multiplier circuits with multiplicand widths in excess of 64 bits. Unfortunately, multipliers with different architectures do not provide enough structural similarity to allow verification with the these methods.
Architectural changes are common, however, and particularly during the earlier part of the design process. For example, with respect to multipliers, it is common to swap one multiplier architecture for another in order to explore design tradeoffs. As a specific example, it would not be uncommon to substitute an array multiplier (as shown in
FIG. 1
) for a Wallace-tree multiplier (as shown in FIG.
2
), or vice versa.
Across different architectures, there are known methods for verification, but only if the verification tool knows that the circuits to be verified are multipliers and also knows how the integers processed by the multiplier are encoded.
It would therefore be desirable to develop a general technique for formally determining equivalence between circuits of different architectures such that it is not necessary for the verification tool to know the particular functionality of the circuits to be compared nor the specific way in which the operands of the circuits are encoded.
SUMMARY OF THE INVENTION
The present invention utilizes a particular type of structural similarity between the reference and implementation designs, which we shall refer to as “structural dependence,” in order to broaden the class of circuits that are formally verifiable in an efficient manner. Structural dependence is the dependence of the higher-order result bits of a design upon the circuitry driving the lower-order result bits.
Because structural dependence is a rather general and high-level characteristic, two circuits which might be considered, according to conventional standards, as having very different structures and therefore not amenable to efficient formal verification, may in fact be efficiently comparable using the present invention.
Structural dependence is utilized in partitioning the two circuits, &eegr; and &eegr;′, to be compared. Each circuit has the fanin cones of its primary inputs ordered from smallest to largest. Each such fanin cone is the basis for forming a circuit partition, but part of a fanin cone may be excluded from a partition to the extent it is already part of another partition.
Structural dependence partitioning creates subcircuits &eegr;
i
for circuit &eegr; and subcircuits &eegr;′
i
for circuit &eegr;′. Each subcircuit (or partition) &eegr;
i
drives a primary output z
i
and each subcircuit (or partition) &eegr;′
i
drives a primary output z′
i
. In addition, each subcircuit &eegr;
i
may have: a fanout set Y
i
to its higher order subcircuit &eegr;
i+1
, (if it has a higher order subcircuit and is connected to it), inputs from the fanout set Y
i−1
of its lower order subcircuit &eegr;
i−1
, (if it has a lower order subcircuit and is connected to it) and primary inputs from X (if it is driven by one or more primary inputs). Likewise, each subcircuit &eegr;′
i
may have: a fanout set Y′
i
to its higher order subcircuit &eegr;′
i+1
(if it has a higher order subcircuit and is connected to it), inputs from the fanout set Y′
i−1
of its lower order subcircuit &eegr;′
i−1
(if it has a lower order subcircuit and is connected to it) and primary inputs from X (if it is driven by one or more primary inputs).
Since the lower order primary output bits have smaller fanin cones with fewer inputs than the higher order bits, they may be verifiable by known techniques. As we proceed toward the higher order bits, however, implicit verification using structural dependence becomes increasingly important.
Implicit verification operates as follows, for example, with respect to verifying the high-order primary output bit of two n bit circuits. While the following discussion is stated with respect to two multiplier circuits being compared, it applies to any two circuits which have been partitioned according
Do Thuan
Howrey Simon Arnold & White , LLP
Kaplan Jonathan T.
Smith Matthew
Synopsys Inc.
LandOfFree
Method and apparatus for implicit verification of digital... 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 apparatus for implicit verification of digital..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and apparatus for implicit verification of digital... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2909202