Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2007-03-28
2010-02-09
Chiang, Jack (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000, C716S030000, C716S030000, C716S030000, C703S013000, C703S014000
Reexamination Certificate
active
07661082
ABSTRACT:
An apparatus and methods for the verification of digital design descriptions are provided. In an exemplary embodiment, a method of verifying a property in a digital design description is provided. The method includes deriving an abstraction of the digital design description, determining a counterexample by an approximate reachable state computation, justifying the counterexample, determining a justification frontier, updating the abstraction from the justification frontier, and producing a verification result for the digital design description. One feature of this embodiment is that it provides for efficient digital circuit verification. This Abstract is provided for the sole purpose of complying with the Abstract requirement rules that allow a reader to quickly ascertain the subject matter of the disclosure contained herein. This Abstract is submitted with the explicit understanding that it will not be used to interpret or to limit the scope or the meaning of the claims.
REFERENCES:
patent: 6587998 (2003-07-01), Rodeh
patent: 7203631 (2007-04-01), Fraer et al.
patent: 7305637 (2007-12-01), Ganai et al.
patent: 2003/0225552 (2003-12-01), Ganai et al.
patent: 2004/0123254 (2004-06-01), Geist et al.
Amla et al, “An Analysis of SAT-Based Model Checking Techniquese in an Industrial Environment”, Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science No. 3725, 2005.
Amla et al, “A hybrid of counterexample-based and proof-based abstraction”, Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science, vol. 3312, 2004.
Awedh et al, “Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States”, University of Colorado at Boulder, available at vlsi.colorado.edu/˜awedh/myPapers/bddsat.pdf.
Biere et al, “Liveness Checking as Safety Checking”, Electronic Notes in Theoretical Computer Science, 66, No. 2, 2002—available at http://www.elseiver.nl/locate/entcs/volume66.html.
Biere et al, “Symbolic Model Checking without BDDS*”, TACAS'99 and ETAPS'99, Amsterdam, The Netherlands, Lecutre Notes in Computer Science, vol. 1579, 1999.
Burch et al, “Symbolic Model Checking 1020 States and Beyond”, Information and Computation, vol. 98, No. 2 Jun. 1992.
Clarke et al., “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic”, E.A. Logics of Programs 1981, Springer Lecture Notes in Computer Science, No. 131, Springer-Verlag, 1982.
Goldberg et al, “BerkMin: a Fast and Robust Sat-Solver”, Design, Automation, and Test in Europe, Mar. 2002.
Gupta et al, “Abstraction Refinement for Bounded Model Checking”, Computer Aided Verification, Leture Notice in Computer Science, vol. 3576, 2005.
Huang et al, “Assertion Checking by Combined Word-level ATPG and Modular Arithmetic Constraint-Solving Techniques”, Design Automation Conference, Issue 37, 2000.
Awedh et al, “Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States”, University of Colorado at Boulder, available at vlsi.colorado.edu/˜awedh/myPapers/bddsat.pdf, Nov. 2004, pp. 1-15.
Iyer et al, “Satori—A Fast Sequential SAT Engine for Circuits”, ICCAD '03, Nov. 11-13, 2003.
Li et al, “Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking”, TACAS, Lecture Notes in Computer Science, vol. 3920, 2006.
Li et al, “Abstraction Refinement in Symbolic Model Checking Using Satisfiability as the Only Decision Procedure”, STTT, vol. 7, No. 2, 2005.
Marques-Silva, J., “Improvements to the Implementation of Interpolant-Based Model Checking”, CHARME, 2005, LNCS 3725, 2005.
Marques-Silva et al, “GRASP: A Search Algorithm for Propositional Satisfiability”, IEEE Transactions on Computers, vol. 48, No. 5, May 1999.
McMillan, K.L., “Interpolation and SAT-Based Model Checking”, Lecture Notes in Computer Science, vol. 2725, 2003.
McMillan et al, “Automatic Abstraction without Counterexamples”, Lecture Notes in Compter Science, vol. 2619, 2003.
Moskewicz et al, “Chaff: Engineering an Efficient SAT Solver”, Proceedings of the 38th conference on Design automation, 2001.
Prasad et al, “A Survey of Recent Advances in SAT-Based Formal Verification”, STTT, vol. 7, No. 2, 2005.
Ravi et al, “Minimal Satisfying Assignments for Bounded Model Checking”, Lecture Notes in Compter Science, vol. 2988, 2004.
Whittemore et al, “SATIRE: A New Incremental Satifiability Engine”, Proc. of the Design Automation Conference, 2001.
Amla Nina
McMillan Kenneth L.
Cadence Design Systems Inc.
Chiang Jack
Doan Nghia M
Townsend and Townsend / and Crew LLP
LandOfFree
System and method for abstraction refinement 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 System and method for abstraction refinement verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System and method for abstraction refinement verification will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-4175639