Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2000-04-20
2001-10-09
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
Reexamination Certificate
active
06301687
ABSTRACT:
BACKGROUND OF THE INVENTION
This invention relates generally to the field of computer-aided design (CAD) systems and methods, and more specifically to methods used for digital circuit design and verification.
Successful design of a complex digital system requires verifying the correctness of the implementation with respect to its intended functionality. Traditionally, the task of design validation is carried out by means of simulation. In a simulation based approach, the designer needs to create a complete set of test vectors which represent all possible inputs to the system. The outputs for each of these test vectors are analyzed to guarantee the correctness of the design. This process is highly Central Processing Unit (CPU) time intensive; in almost all practical situations it is not feasible to exhaustively simulate a design to guarantee its correctness.
Due to the limitations of a simulation based approach, various formal verification strategies are becoming increasingly popular. By using these techniques, it is possible to guarantee the correctness of a design under all possible input combinations.
The process of designing a complex system usually starts with an abstract model of the system. This model is subjected to extensive simulation after which it becomes the “golden specification” of the design. From this abstract model, a detailed implementation is derived in a hierarchical manner. First the abstract model is translated into a synthesizable, behavioral Register Transfer Level (RTL) model representing the block structure behavior of the design. This behavioral RTL model is then translated into a structural model which is a logic level description of the system. From the structural RTL model a transistor netlist and subsequently the physical layout of the design are derived.
In a successful design methodology, it is essential to catch design errors early in the design cycle. To achieve this goal, the functionality of the design is verified at every level of the design cycle hierarchy against a design specification from the previous level. This kind of formal verification in which different implementations of the same design are compared to check their equivalence is known as implementation verification.
FIG. 1
is a prior art flow diagram of a typical verification effort. Note that the verification effort may be carried out in parallel with the design effort. The typical verification effort starts by verifying the first implementation against the original specification. Once an implementation has been verified successfully, it becomes the specification for the next implementation, which is typically derived by optimizing the previous implementation. The first or original design is represented as RTL design
10
and optimized
12
to produce optimized RTL design
14
. The optimized RTL is verified against the first RTL by verify
1
16
. The optimized RTL is synthesized
18
to produce a gate-level netlist
20
. The gate-level netlist is verified against the optimized RTL by verify
2
22
. The gatelevel netlist is optimized
24
to produce an optimized netlist. The optimized netlist is verified against the gate-level netlist by verify
3
28
. Next, test logic is added
30
to the optimized netlist to create a modified netlist
32
. The modified netlist is verified against the optimized netlist by verify
4
34
. The modified netlist is placed and routed
36
to produce a final netlist
38
. Finally, the final netlist is verified against the modified netlist by verify
5
40
.
Implementation verification typically proceeds in two phases. In the first phase, a Boolean network representing the original design is extracted from the RTL description or the gate-level netlist. In the second phase, the correctness of this Boolean network is verified using formal methods.
Current research is focused on making advances in the area of verifying the equivalence of two Boolean networks. More specifically, research is focused on the verification of combinational circuits, i.e., circuits in which the outputs depend only on the current inputs (as opposed to sequential circuits in which the outputs depend not only on the present inputs but also on the past sequence of inputs). Some sequential verification problems can be reduced to a combinational verification problem (e.g., when the corresponding latches in the two designs can be identified). Although techniques exist for verifying general sequential circuits, it is not practical with current technology to verify large complex circuit designs using the techniques.
The combinational verification problem can be stated as follows. Given two Boolean netlists, check if the corresponding outputs of the two circuits are equal for all possible inputs. This problem is NP-hard and hence a general solution which can handle arbitrary Boolean functions is not likely to exist. However, since the functions that are implemented in the circuit design in practice are not random Boolean functions, various techniques have been developed which can successfully verify large designs.
The work in combinational equivalence checking can be classified into two main categories. The first approach consists of representing the output functions of the two networks using a unique (i.e. canonical) representation. Two circuits are equivalent if and only if the canonical representations of the corresponding outputs are the same. The most popular canonical representations are based on Binary Decision Diagrams (BDDs). In the worst case, these methods can require exponential space (in terms of the number of inputs).
The second approach consists of identifying equivalent points and implications between the two circuits. Using this information, the process of equivalence checking can be simplified. Since a typical design proceeds by a series of local changes, in most cases there are a large number of implications between the two circuits to be verified. These implication based techniques have been very successful in verifying large circuits and form the basis of most combinational verification systems.
Most current methods for combinational verification are based on a single “core” verification technique such as OBDDs, automatic test pattern generation (ATPG), learning etc. A core verification technique is a technique that is capable by itself to verify a circuit or prove tautology or satisfiability of some Boolean formula given enough time and space. A core verification technique is also known as a complete analysis technique, that is, a technique that is capable by itself to prove tautology or satisfiability of some Boolean formula given enough time and space. In contrast, a supporting analysis technique is a technique that, when used by itself, can detect tautology or satisfiability of some but not all Boolean formulas even when given enough time and space. Due to the NP-hard complexity of the verification problem, it is expected that a single core verification technique will not perform well on a wide range of circuits. In addition, the nature of any given verification problem is not known a priori. This uncertainty is further worsened in some verification techniques because the entire verification problem may be broken down into even more (though smaller) verification problems. Thus, there is a need for methods which can employ different core verification techniques automatically, with minimal overhead in switching from one technique to the other, while sharing the results of the previously applied techniques, and which provide verification results when any one or more of the techniques can be successful.
SUMMARY OF THE INVENTION
The present invention is a filter based combinational circuit verification system having a set of complete verification techniques along with a set of supporting techniques, arranged sequentially, each determining the result of verification or altering the circuit data structure, and executed until a predetermined set of constraints on the computer memory usage and/or the computer execution time usage are exceeded, and providing the final ver
Jain Jawahar
Mukherjee Rajarshi
Takayama Koichiro
Christie Parker & Hale LLP
Fujitsu Limited
Garbowski Leigh Marie
Smith Matthew
LandOfFree
Method for verification of combinational circuits using a... 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 verification of combinational circuits using a..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method for verification of combinational circuits using a... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2581140