Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1999-09-27
2002-01-01
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000, C716S030000, C716S030000, C703S015000
Reexamination Certificate
active
06336206
ABSTRACT:
FIELD OF THE INVENTION
The present invention relates generally to circuit design verification, and more particularly to structural circuit design verification.
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. In particular, 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).
Formality operates by identifying “compare points” which are points in the reference and implementation designs that are examined for equivalency. If all compare points in the implementation design are found equivalent to a corresponding compare point in the reference design, then the two designs are, in total, equivalent to each other.
Three major components comprise the Formality architecture: a verification manager, a suite of verification solvers and a debug analyzer. The verification manager is responsible for determining the corresponding compare point of the reference design that should be compared for functional equivalency against each compare point of the implementation design. The verification manager also determines the logic cone for each compare point. The logic cone for each compare point is found by following each compare point's transitive fanin until a primary input, or another compare point, is reached. These primary inputs or compare points, which define the transitive fanin boundary of a compare point, shall be referred to as the compare point's logic cone inputs. In addition to determining the corresponding compare point of the reference design, for each compare point of the implementation design, the verification manager also “aligns” the logic cone inputs for such paired compare points. The verification manager accomplishes this by determining the logic cone input of the reference design's compare point, that should be correspond to each logic cone input of the implementation design's compare point, when functional equivalency of the compare points for the two logic cones is being determined.
Once such compare point matching and logic cone input alignment has been determined, algorithms to determine equivalency can be applied. Formality chooses the most appropriate equivalency-determining algorithm (referred to as a “solver”) from its suite of verification solvers. For example, a binary decision diagram (BDD) based solver may be used for compare points driven by complex control logic, but other algorithms may be more efficient for data path circuits.
Equivalency of two combinational circuits can be defined, in a functional sense, as follows. The reference and implementation designs are equivalent if both accept the same set of input combinations, and if both produce the same output combination for each input combination. Equivalency can also be defined, in a less strict sense, if don't cares are allowed in the reference design's input combinations. In that case, the implementation design only needs to define the same function over those input patterns for which the reference design is defined.
If Formality discovers errors during the verification process, the designer can identify nets or instances of the implementation design that may be responsible for the errors with the Formality debug analyzer.
Determining the corresponding compare points between the reference and implementation designs, and aligning the logic cone inputs of the compare points, is important for formal verification systems, such as Formality, since it permits the relatively computationally expensive equivalency-determining algorithms to be strategically applied. It would therefore be desirable to improve the speed and specificity with which such compare point correspondences, and logic cone alignments, can be found.
SUMMARY OF THE INVENTION
For purposes of describing the present invention, the determination of compare point correspondences, and logic cone input alignments, shall be referred to as the determination of “necessary correspondences” between inputs or outputs of the two circuits to be compared. A necessary correspondence between a first output of a first circuit and a first output of a second circuit indicates that both the following statements are true: i) if the first output of the first circuit is equivalent to an output of the second circuit, then that equivalent output must be the first output of the second circuit; and ii) if the first output of the second circuit is equivalent to an output of the first circuit, then that equivalent output must be the first output of the first circuit. A necessary correspondence between a first input of a first circuit and a first input of a second circuit indicates that both the following statements are true: i) if the first input of the first circuit is equivalent to an input of the second circuit, then that equivalent input must be the first input of the second circuit; and ii) if the first input of the second circuit is equivalent to an input of the first circuit, then that equivalent input must be the first input of the first circuit. These necessary correspondences are so called because while they establish necessary conditions for equivalency to occur, they are not sufficient to determine that equivalency actually exists.
Once such necessary correspondences have been determined, algorithms to determine actual equivalency can be more strategically applied. The present invention comprises a method for determining such necessary correspondences in an efficient way such that the cost of utilizing it is often much smaller than the cost of utilizing equivalency-determining methods. Therefore, it is often cost-effective (i.e. more efficient), as part of an equivalency-determining circuit design tool, to first apply the teachings of the present invention in order to lessen subsequent application of an equivalency determining method.
The present invention presents an efficient method for finding necessary correspondences between the combinational portions of two circuit designs util
Howrey Simon Arnold & White , LLP
Kaplan, Esq. Jonathan T.
Kik Phallaka
Smith Matthew
Synopsys Inc.
LandOfFree
Method and apparatus for structural input/output matching... 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 structural input/output matching..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and apparatus for structural input/output matching... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2853450