Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2002-04-04
2004-07-13
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000, C716S030000, C716S030000
Reexamination Certificate
active
06763505
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Technical Field
The present invention is directed to an apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs.
2. Description of Related Art
Functional hardware verification is the process of demonstrating the correct behavior of a hardware design. Typically, the verification is performed on a “software” model of the design, e.g., the hardware description language (HDL), or a netlist representation derived through compilation of the HDL or custom design (or some other “compiled” format), which is executed on a computer or downloaded onto a hardware emulator. A trace of the “software” model is generated by a verification tool and may be used to expose any problems in the software model or provide an output to a human user that may use the trace to evaluate the correctness of the design during operation.
A trace may be, for example, an “all events trace” that illustrates 0, 1 valuations to each gate of a software model over time. Such traces can be created by simulation tools evaluating the software model in response to a test case, e.g., sequences of 0, 1 values of the input to the software model over time, or by formal verification algorithms which are commonly referred to as “counterexample traces.”
The size of the design under test represents a significant bottleneck for the necessary verification resources. For simulation and emulation test-based techniques, the required resources are nearly linear with respect to design size. The drawback of such test-based techniques is that they are incomplete, and cannot prove the absence of design flaws, only their presence. Consequently there has been a peak of interest in formal verification techniques, which can prove the absence as well as presence of design flaws. However, such techniques consume exponential verification resources with respect to design size. In particular, verification resources typically run exponential with respect to the number of sequential elements (e.g., latches or registers) in the design. Combinational optimization techniques, prevalent in both test-based and formal verification paradigms, are capable of significantly reducing design size, but are limited in applicability to only the logic between sequential element boundaries. Thus sequential elements limit the ability of combinational model reduction techniques to simplify designs for verification regardless of the verification paradigm.
One technique, known as phase abstraction, has been developed to help minimize the number of sequential elements in a design under test. The use of phase abstraction for enhanced verification has been noted in several publications including “Efficient Equivalence Checking of Multi-Phase Designs Using Phase Abstraction and Retiming,” G. Hasteer, A. Mathur, and P. Banerjee, in Proceedings of the High-Level Design Validation and Test Symposium 1997 (which focusses on sequential hardware equivalence checking) and “Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists,” J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz, in Proceedings of the Conference on Computer-Aided Verification 1999 (which focusses on functional verification), which are hereby incorporated by reference. In addition, a specific technique for performing phase abstraction is described in commonly assigned U.S. Pat. No. 6,321,184, which is also hereby incorporated by reference. In particular, for a design composed of level-sensitive latches, phase abstraction converts all but one “class” of latches to wires based on the fact that the latches are transparent when they are clocked. The remaining class of latches is converted to registers, thereby significantly reducing the number of sequential elements by at least a factor of “k” for a “k”-phase design.
The impact of this technique on increasing the power of combinational optimization techniques, and on increasing the speed with which verification algorithms operate (basically linear for test-based techniques, and exponential for formal verification techniques), has been previously noted above. However, this technique has several complications and unpleasant side effects.
First, one must provide the glue to partition the latches into various classes. In other words, the user of the phase abstraction technique must identify which latches are of a particular type in order for the phase abstraction to work. Thus, an additional burden is placed on the user of the phase abstraction technique. Moreover, if the determination of latch type is incorrect, verification of the phase abstracted netlist becomes unsound, i.e. the verification results obtained on the phase abstracted netlist may not imply anything about correctness of the original netlist.
Second, design techniques such as gated-clock latches provide complications for these techniques. During phase abstraction, if a gated clock latch is replaced by a wire, the resulting trace includes errors due to the fact that the latch is not always transparent during the latch's clocking at which it is normally transparent. This is because a gate signal may be used to alter the operation of the latch during this clocking. In particular, the global clock of the netlist can be selectively stopped for gated-clock latches by ANDing this global clock with a gate signal before driving it to these latches. As a result, if phase abstraction eliminates such latches, their gated behavior is destroyed, i.e. when their gates “close” they will still appear to behave as if their gates were “open.” Thus, phase abstraction in the presence of gated-clock latches also risks making the transformation unsound for verification purposes.
Third, any simulation-style of traces obtained on a phase abstracted design will be in terms of the phase-abstracted model itself, which may be unattractive to those who expect a trace in terms of the original model. It may be difficult and time consuming for the human user of the phase abstraction technique to convert the trace obtained through phase abstraction into a corresponding trace that would have been obtained without the phase abstraction.
Thus, it would be beneficial to have an apparatus and method for eliminating these three unattractive side-effects and/or complications of phase abstraction and thereby, provide a truly seamless or “invisible” automatic use of phase abstraction for enhanced verification.
SUMMARY OF THE INVENTION
The present invention provides an apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs. With the apparatus and method of the present invention latches are “colored,” i.e. classified into different types, based on information obtained from a clock tree of the circuit design. In the clock tree, clock tree primitives drive all clock signals to the latches. These clock tree primitives contain sufficient information to taxonomize the clocks into their respective phases. This information may further be used to identify which latches are gated latches.
In coloring the latches, in a preferred embodiment, gated latches are replaced in the circuit design with a free running clock, a multiplexor, and a sequence of L1 to Ln latches to provide a feedback path via the data path. This allows the gated latch to be phase abstracted without losing the “gated” functionality of the gated latch in the resulting trace.
Once the latches are colored in this way, phase abstraction is performed on the colored circuit design. The phase abstracted netlist is then subjected to verification, e.g., simulation, or formal verification. As a result of the verification, a trace may be produced. This trace will be in terms of the phase abstracted circuit, since verification was performed upon the phase abstracted circuit. The coloring information of the original circuit, plus information as to the exact nature of the phase abstraction performed, is then used to transform the phase abstracted trace to one which resembles a trace of the circuit without phase abstraction.
To und
Baumgartner Jason Raymond
Kanzelman Robert Lowell
Roesner Wolfgang
Dimyan Magid Y.
Tkacs Stephen R.
Yee Duke W.
LandOfFree
Apparatus and method for automated use of phase abstraction... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Apparatus and method for automated use of phase abstraction..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Apparatus and method for automated use of phase abstraction... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3217520