Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2000-12-11
2003-05-13
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000
Reexamination Certificate
active
06564358
ABSTRACT:
FIELD
The present invention relates to the field of computer systems, and more specifically to a method and system for formal verification of a circuit model.
BACKGROUND
One method of verifying a circuit design is called formal verification. Formal verification is the use of mathematical techniques to formally (i.e. without simulating circuit input vectors) compare circuit design models which are at different levels of abstraction to establish logic functionality equivalence between the two models. For example, formal verification is used to compare the specification of a logic circuit in some hardware description language (HDL) against its implementation as a schematic model.
Formal verification tools are often based on binary decision diagrams (BDDs). BDDs are directed acyclic graph structures that encode the value of a boolean logic function for all possible input value combinations. BDDs simplify the task of boolean function equivalence, since BDDs have efficient algorithms for equivalence checking and other boolean operations.
However, BDD techniques suffer from exponential memory requirements since the size of the BDD representing a given circuit can grow exponentially relative to the inputs of the circuit. To overcome this, solutions based on a divide-and-conquer approach have been developed. These techniques attempt to partition the specification and implementation circuit models along frontiers of equivalent signal pairs called cut-points. The resulting sub-circuit partitions of each circuit model are independently analyzed, thus breaking the verification task into manageable units.
However, one problem that arises when introducing cut-points into circuit models is that the verification method may return a false negative. False negatives appear when the technique that compares the two circuits classifies them as different, while in reality they are not. Thus, cut-point based formal verification techniques include a process of eliminating false negatives by attempting to determine whether the corresponding circuit outputs are truly different or the algorithm produced a false negative. This extra step is time-consuming.
Accordingly, for the reasons stated above, and for other reasons stated below which will be appreciated by those skilled in the art upon reading and understanding the present specification, there is a need in the art for a method of verifying circuit models which is faster and permits the verification of more complex circuits within a formal mathematical framework.
REFERENCES:
patent: 5754454 (1998-05-01), Pixley et al.
patent: 5937183 (1999-08-01), Ashar et al.
patent: 6035107 (2000-03-01), Kuehlmann et al.
C. Leonard Berman et al., Functional Comparison of Logic Designs for VLSI Circuits, 1989 IEEE International Conference on Computer-Aided Design, pp. 456-459, Nov. 1989.*
F. Krohm et al., The Use of Random Simulation in Formal Verification, 1996 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 371-376, Oct. 1996.*
Z. Khasidashvili et al., An Enhanced Cup-Points Algorithm in Formal Equivalence Verification, 6thIEEE International High-Level Design Validation and Test Workshop, pp. 171-176, Nov. 2001.*
R. Mukherjee et al., Efficient Combinational Verification Using BDDs and A Hash Table, 1997 IEEE International Symposium on Circuits and Systems, pp. 1025-1028, Jun. 1997.*
Z. Khasidashvili et al., An Enhanced Cut-points Algorithm in Formal Equivalence Verification, 6th IEEE International High-Level Design Validation and Test Workshop, pp. 171-176, Nov. 2001.*
Bryant, R.E., “Graph-Based Algorithms for Boolean Function Manipulation”,IEEE Transactions on Computers, C-35 (8), pp. 677-691, (1986).
Fujita, M., et al., “Evaluation and Improvement of Boolean Comparison Method base on binary decision diagrams”,IEEE Internationa Conference on Computer-Aided Design, ICCAD-88 Digest of Technical Papers, 2-5, (Nov. 1988).
Kuehlman, A., et al., “Equivalence Checking Using Cuts and Heaps”,34th Design and Automation Conference Proceedings, (1997).
Matsunaga, Y., “An Efficient Equivalence Checker for Combinational Circuits”,33rd Design and Automation Conference proceedings 1996, 629-634, (1996).
Reddy, S.M., et al., “Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment”,32 Design Automation Conference Proceedings 1995, 414-419, (1995).
Rudell, R., “Dynamic Variable Ordering for Ordered Binary Decision Diagrams”,1993 IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, IEEE Comput. Soc. Press, 42-47, (Nov. 1993).
Hanna Ziyad
Kaiss Daher Adil
Moondanos John
Seger Carl J.
Schwegman Lundberg Woessner & Kluth P.A.
Smith Matthew
Thompson A. M.
LandOfFree
Method and system for formal verification of a circuit model... 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 system for formal verification of a circuit model..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and system for formal verification of a circuit model... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3071831