Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2002-11-07
2004-09-14
Siek, Vuthe (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000
Reexamination Certificate
active
06792581
ABSTRACT:
FIELD
An embodiment of the present invention relates to the field of integrated circuit formal equivalence verification, and, more particularly, to an approach for determining a cut-point frontier and/or for counter-example generation.
BACKGROUND
Formal verification typically employs the use of mathematical techniques to “formally” (i.e. without simulating circuit input vectors) compare two circuit design models at the same or differing levels of abstraction to verify logic functionality equivalence between the models. For example, a formal equivalence verification process may be used to compare a logic circuit model in some hardware description language (HDL) against its implementation as a corresponding schematic model at the transistor level. The circuit model at the higher level of abstraction will be referred to herein as the specification circuit model (or spec) while the one at the lower level of abstraction will be referred to herein as the implementation circuit model (or imp).
Formal equivalence verification tools are frequently based on classical binary decision diagrams (BDDs). Classical BDDs are directed acyclic graph structures that encode the value of a Boolean logic function for all possible input value combinations. BDDs, in general, simplify the task of determining Boolean function equivalence because efficient algorithms for equivalence checking and other Boolean operations exist for BDDs. Because the size of a BDD representing a given circuit can grow exponentially larger with respect to the number of inputs and gates in the circuit, the memory requirements for using a formal equivalence verification tool that employs a classical BDD approach may be prohibitively large.
To address this issue, solutions using a divide-and-conquer approach have been developed. Such 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 then independently analyzed such that the verification task is broken into more manageable units. The manner in which cut-points and/or cut-point frontiers are selected can affect the performance of the associated formal equivalence verification tool.
One problem that may arise for some prior formal verification tools when introducing cut-points into circuit models is that the verification method may return a false negative. A false negative in this context is an indication by the formal equivalence verification tool that two circuits are different, when in reality, they are not. The process of eliminating false negatives can be time consuming.
Further, when a difference between two circuit models is identified, such prior tools typically do not provide the integrated circuit designer with information as to the source of the differences between two circuit models.
REFERENCES:
patent: 5202889 (1993-04-01), Aharon et al.
patent: 5331568 (1994-07-01), Pixley
patent: 5544067 (1996-08-01), Rostoker et al.
patent: 5724504 (1998-03-01), Aharon et al.
patent: 5748497 (1998-05-01), Scott et al.
patent: 5754454 (1998-05-01), Pixley et al.
patent: 5801958 (1998-09-01), Dangelo et al.
patent: 5937183 (1999-08-01), Ashar et al.
patent: 6006028 (1999-12-01), Aharon et al.
patent: 6035107 (2000-03-01), Kuehlmann et al.
patent: 6035109 (2000-03-01), Ashar et al.
patent: 6086626 (2000-07-01), Jain et al.
patent: 6195788 (2001-02-01), Leaver et al.
patent: 6212669 (2001-04-01), Jain
patent: 6269467 (2001-07-01), Chang et al.
patent: 6301687 (2001-10-01), Jain et al.
patent: 6308299 (2001-10-01), Burch et al.
patent: 6334205 (2001-12-01), Iyer et al.
patent: 6378112 (2002-04-01), Martin et al.
patent: 6408424 (2002-06-01), Mukherjee et al.
patent: 6449750 (2002-09-01), Tsuchiya
patent: 6564358 (2003-05-01), Moondanos et al.
patent: 2001/0025369 (2001-09-01), Chang et al.
patent: 2002/0073380 (2002-06-01), Cooke et al.
patent: 2002/0108093 (2002-08-01), Moondanos et al.
patent: 2002/0144215 (2002-10-01), Hoskote et al.
patent: 2003/0200073 (2003-10-01), Rich et al.
C. Leonard Berman, Louise H. Trevillyan, “Functional Comparsion of Logic Designs for VLSI Circuits”, 1989 IEEE, pp. 456-459.
Masahiro Fujita, Hisanori Fujisawa, Nobuaki Kawato, “Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams”, 1988 IEEE, pp. 2-5.
Florian Krohm, Andreas Kuehlmann, Arjen Mets, “The Use of Random Simulation in Formal Verification”, 1996 IEEE, pp. 371-376.
Richard Rudell, “Dynamic Variable Ordering for Ordered Binary Decision Diagrams”, 1993 IEEE, pp. 42-47.
Andreas Kuehlmann, Florian Krohm, “Equivalence Checking Using Cuts and Heaps”, pp. 263-268.
Rajarshi Mukherjee, Jawahar Jain, Koichiro Takayama, Masahiro Fujita, Jacob A. Abraham, Donald S. Fussell, Efficient Combinational Verification Using BDDs and a Hash Table, 1997 IEEE, Jun. 9-12, 1997, Hong Kong, pp. 1025-1028.
Elena Dubrova, Luca Macchiarulo, “A Comment on Graph-Based Algorithm for Boolean Function Manipulation”, 2000 IEEE, vol. 49, No. 11, Nov. 2000, pp. 1290-1292.
Subodh M. Reddy, Wolfgang Kunz, Dhiraj K. Pradhan, “Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment”, 1995 ACM 0-89791-756-1/95/0006, pp. 1-6.
Randal E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation12”, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA 15213, table of contents and pp. 1-25.
Yusuke Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits”, Fujitsu Laboratories Ltd., Kawasaki 211-88, Japan, 41.1, pp. 629-634.
Paruthi et al., “Equivalence Checking Combing a Structural SAT-solver, BDDs, and Simulation”, Proceedings of 2000 International Conference on Computer Design, Sep. 17, 2000, PP. 459-464.
Huang et al., “Aquila: An Equivalence Verifier for Large Sequential Circuits”, Proceedings of the ASP-DAC '97 Asian and South Pacific Design Automation Conference, Jan. 28, 1997, pp. 455-460.
Rho et al., “Inductive Verification of Iterative Systems”, Proceedings of 29thACM/IEEE Design Automation Conferences, Jun. 8, 1992, pp. 628-633.
Krohm et al., “The Use of Random Simulation in Formal Verification”, Proceedings of 1996 IEEE International Conference on Computer Design: VLSI in Computers and Processors, Oct. 7, 1996, pp. 371-376.
Hanna Ziyad E.
Khasidashvili Zurab
Moondanos John
Faatz Cynthia T.
Intel Corporation
Siek Vuthe
Tat Binh
LandOfFree
Method and apparatus for cut-point frontier selection and... 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 cut-point frontier selection and..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and apparatus for cut-point frontier selection and... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3232917