Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2007-12-18
2007-12-18
Garbowski, Leigh M. (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000
Reexamination Certificate
active
10309529
ABSTRACT:
Processes for formal verification of circuits and other finite-state systems are disclosed. For one embodiment, a process is disclosed to provide for significantly reduced computation through automated symbolic indexing of a property assertion and to compute the satisfiability of the property assertion directly from a symbolic simulation of the indexed property assertion. For an alternative embodiment a process using indexed property assertions on a symbolic lattice domain to represent and verify properties, provides an efficient symbolic manipulation technique using binary decision diagrams (BDDs). Methods for computing symbolic simulations, and verifying satisfiability may be applicable with respect to property assertions that are symbolically indexed under specific disclosed conditions. A process is also disclosed to compute a constraint abstraction for a property assertion, thereby permitting automated formal verification of symbolically indexed properties under constraints and under specific conditions, which may be automatically checked.
REFERENCES:
patent: 6163876 (2000-12-01), Ashar et al.
patent: 6339837 (2002-01-01), Li
patent: 6378112 (2002-04-01), Martin et al.
patent: 6484134 (2002-11-01), Hoskote
patent: 6539345 (2003-03-01), Jones et al.
patent: 6567959 (2003-05-01), Levin et al.
patent: 6591400 (2003-07-01), Yang
patent: 6643827 (2003-11-01), Yang
patent: 6725431 (2004-04-01), Yang
patent: 6931611 (2005-08-01), Martin et al.
patent: 2004/0107174 (2004-06-01), Jones et al.
“Abstraction by Symbolic Indexing Transformations”, T. F. Melham et al., Proceedings of the 4th Int. Conference on Formal Methods in Computer-Aided Design, Nov. 6-8, 2002.
“A Methodology for Hardware Verification Based on Logic Simulation”, Randal E. Bryant, Journal of the Ass. for Computing Machinery, vol. 38, No. 2, Apr. 1991, pp. 299-328.
“Formal Verification of Content Addressable Memories using Symbolic Trajectory Evaluation”, Pandey M. et al., ACM 1997.
“Functional Verification of Multi-Million Gates ASICs for Designing Communications Networks: Trends, Tools and Techniques”, MK Dhodhi et al., Microelectronics, 1999. ICM '99.
“Formal Verification of PowerPC arrays using symbolic trajectory evaluation”, M. Pandey et al., ACM Proceedings of the 33rd Annual Conf. on Design Automation, pp. 649-654, 1996.
“A Simple Theorem Prover Based on Symbolic Trajectory Evaluation and BDD's”, S. Hazelhurst et al., IEEE Trans. of Computer-Aided Design of Integrated Circuits and Systems, vol. 14, No. 4, Apr. 1995.
“Success-Driven Learning in ATPG for Preimage Computation”, S. Sheng et al., IEEE Design & Test of Computers, pp. 504-512, Nov.-Dec. 2004.
“Practical Formal Verification in Microprocessor Design”, R. B. Jones et al., IEEE Design & Test of Computers, pp. 16-25, Jul.-Aug. 2001.
MK Dhodhi et al., Functional Verification of Multi-Million Gates ASICs for Designing Communications Networks: Trends, Tools and Techniques, Microelectronics, 1999. ICM '99.
S. Sheng et al., Success-Driven Learning in ATPG for Preimage Computation, IEEE Design & Test of Computers, pp. 504-512, Nov.-Dec. 2004.
Aagaard, Mark D., et al., “Formal Verification Using Parametric Representations of Boolean Constraints”, Strategic CAD Labs, Intel Corporation, Hillsboro OR 97124 USA, 6 pages. DAC 1999, New Orleans, Louisiana.
Melham, Thomas F. and Jones, Robert B., “Abstraction by Symbolic Indexing Transformations”, 14 pages, Lecture Notes in Computer Science, 2002 (2517) ISSN: 030229743 UCM Biblioteca Compulutense.
Yang, Jin and Tiemeyer, Andreas, “Lazy Symbolic Model Checking”, 4 pages 37thDAC Session 2.3 S, LA Technical Program, Tuesday, Jun. 6, 2000, Los Angeles Convention Center.
Jones Robert B.
Melham Thomas F.
Garbowski Leigh M.
Intel Corporation
Mennemeier Larry M.
LandOfFree
Automatic symbolic indexing methods for formal verification... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Automatic symbolic indexing methods for formal verification..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automatic symbolic indexing methods for formal verification... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3869126