Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2000-08-23
2003-08-26
Siek, Vuthe (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000, C716S030000, C716S030000, C716S030000, C716S030000, C712S001000, C703S014000, C703S028000, C702S109000, C702S123000
Reexamination Certificate
active
06611947
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Field of the Invention
The present invention relates to the field of hardware circuit verification, specifically to verifying identical functionality between two different logic level circuit models. In particular, it relates to a logic verification method that uses a distributed computing environment to quickly solve difficult verification problems.
2. Background of the Related Art
Recent increases in the complexity of modem integrated circuits have resulted in corresponding increases in the difficulty of verifying design correctness. Design flaws have significant economic impact both in terms of increased time-to-market and in reduced profit margins. A typical design flow has many steps, each of which can introduce design flaws. Traditionally, simulation-based techniques have been used to verify design correctness. These techniques have become less effective because of their inability to completely and quickly verify large designs. An increasing popular alternative is the use of formal mathematical techniques, employed by tools known as equivalence checkers, to verify design correctness.
A typical design flow where an integrated circuit is taken from concept to fabrication includes a number of steps. As a first step, the conceptual nature of the integrated circuit is determined. The desired functionality of a circuit is described by a set of specifications. A conceptual model of the circuit is created based on the specifications. For example, in the case of a complex microprocessor, the conceptual nature of the circuit is typically specified in a high level language such as C++. Modeling tools are available which simulate the behavior of the conceptual model under specific test cases to ensure that the model performs as expected.
Once the conceptual nature of the circuit is determined, a register transfer level (RTL) model of the digital circuit is built based upon the conceptual model and is modeled on a digital computer using an RTL modeling tool. At this stage, the design of the circuit, as modeled by the RTL modeling tool, may be used to verify that the circuit meets the desired specifications. In some cases the RTL modeling tool may allow the validity of the modeled circuit to be checked in the context of the high-level language model.
After the design of the RTL model is completed, it is transformed into a gate level model in which individual logic gates are specified and connected together to perform the same logic functions as the RTL level circuit model. The transformation process is error-prone due to both human error and tool error. To validate the transformation, the logic functions of the gate level model must be verified to be the same as the corresponding functions in the RTL model. An equivalence checking tool, such as one described in this invention, can be used to perform this verification.
The gate level model is often further transformed by optimizations that attempt to improve the performance of the circuit such as reducing the area required to construct the circuit, increasing the speed of operation of the circuit and reducing the power consumption of the circuit. Once the gate level logic of the circuit model has been optimized, the optimized gate level model operation must be verified with respect to either the RTL level model or the original gate level model.
The gate level model may go though additional transformations, each yielding successive versions of the circuit. An example of this transformation is scan logic insertion, which allows the circuit to perform in a scan mode and a normal mode. When operating in scan mode the circuit can be tested for manufacturing defects, while in normal mode the circuit should behave as before. Another example is clock tree insertion, which is the process of inserting buffers in the clock tree to improve the timing of clock signals.
At some stage the gate level circuit is placed and routed into a layout. This step may involve further transformations and local optimizations that are driven by placement and timing constraints. Each transformation necessitates the verification of functionality of the pretransformation version compared with the post-transformation version of the circuit.
Conventional equivalence checking tools can be used to verify the functional equivalence of each pre-transformation version versus the corresponding post-transformation version. The verification can be performed by comparing the post-transformation version with either the first RTL circuit model or with a previously verified pre-transformation version. Significant resources (engineering time, computer time and computer memory) are used to perform this verification. Conventional equivalence checking tools frequently fail to complete because of these resource limitations.
In conventional circuit verification, equivalence checking of two circuits is performed by (1) partitioning the two circuits into corresponding combinational subcircuit pairs that contain no storage elements, and (2) sequentially verifying the equivalence of each corresponding subcircuit pair. The circuits are partitioned at circuit inputs, outputs and storage element boundaries. The combinational subcircuit pairs are associated according to a correspondence between the circuit inputs, outputs and storage elements of the two circuits, so that the equivalence is verified for each corresponding set of subcircuits. The conventional device can create the circuit input, output and storage element correspondence with user guidance or automatically—see, e.g., U.S. Pat. No. 5,638,381 to Cho et al., U.S. Pat. No. 5,949,691 to Kurosaka et al. and Foster, “Techniques for Higher-Performance Boolean Equivalence Verification”, Hewlett-Packard Journal 30-38 (August 1998).
Checking identical functionality of combinational subcircuit pairs is an inherently difficult problem. The resources used to perform the check are typically related to the structural differences of the two circuit models. Conventional equivalence checking tools often encounter combinational subcircuit pair checks that cannot be resolved with the allotted time and memory resources.
An example of this difficulty occurs when a combinational subcircuit contains a multiplier. Circuits containing multipliers are well known to be difficult from an equivalence checking perspective—see, e.g., Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 677-691. A standard method of addressing this shortcoming is for the user to intervene and manually partition each combinational subcircuit into two subparts. One subpart of each circuit model contains the multiplier and the other subpart the remainder of the circuit model. The multipliers are typically compared using traditional simulation based methods, while the other subparts can be compared using the conventional equivalence checking tool. The user must take care to partition the combinational subcircuits correctly, and must perform two different equivalence checks to compare the corresponding subparts. The technique of resolving difficult pair checks by splitting the combinational subcircuits into corresponding subparts can be applied to pair checks that do not involve multipliers as well.
Another method of resolving difficult pair checks is to perform case analysis. An illustrative example of a case analysis follows. First, an input to the difficult combinational subcircuit pair is chosen. Then two additional combinational subcircuit pairs are created; one in which the chosen input is assigned to the false value (0), and another in which the chosen input is assigned to the true value (1). Then each corresponding pair is compared using a conventional equivalence checking tool. The user must take care to assign the chosen inputs correctly and must perform two different equivalence checks.
Existing semiconductor design environments typically have significant distributed computing resources available. A design engineer often has convenient access to many wor
Aziz Adnan
Higgins Joseph E.
Singhal Vigyan
Jasper Design Automation, Inc.
Pillsbury & Winthrop LLP
Rossoshek Helen
Siek Vuthe
LandOfFree
Method for determining the functional equivalence between... 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 for determining the functional equivalence between..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method for determining the functional equivalence between... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3129656