Lazy symbolic model checking

Details Lazy symbolic model checking Lazy symbolic model checking

2000-06-30

2004-04-20

Garbowski, Leigh M. (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000

Reexamination Certificate

active

06725431

ABSTRACT:

FIELD OF THE INVENTION
This invention relates generally to automated design verification, and in particular to efficient use of binary decision diagrams to perform automated symbolic model checking for very large scale integrated circuit designs and other finite state systems.
BACKGROUND OF THE INVENTION
Modern design of very large-scale integrated circuits often involves years of research and the efforts of hundreds of engineers. Automated formal verification methods are an essential part of the design effort, reducing errors, lost time and risk to financial investment.
As the size and complexity of designs increase, much effort is expended to improve the efficiency of automated formal verification methods. One technique used in symbolic model checking to improve efficiency is to employ binary decision diagrams (BDDs). A BDD is a directed acyclic graph that represents a Boolean expression. For each Boolean variable, there are two outgoing edges representing true or false assignments to the variable. The use of BDDs permits computation times, which are some polynomial function of the number of expression variables. Alternative representations such as clauses or truth tables require execution times, which are some exponential function of the number of expression variables. Therefore, use of BDDs has been popular in the formal verification community since the late 1980's.
BDDs, however, are not without drawbacks. The ordering of variables is critical to an efficient use of BDDs. Poor variable ordering can increase a BDDs size and cause exponential execution times. One method for symbolic model checking using BDDs comes from Carnegie Mellon University and is known as Symbolic Model Verify (SMV).
Over the years, techniques have been developed to improve performance and capacity of BDD-based algorithms. One technique is called Cone of Influence (COI) reduction. In COI reduction, an abstraction is built for a circuit model consisting of next state functions only for variables in the dependency closure of variables of interest in the circuit specification. One drawback is that all variables in the dependency closure do not necessarily influence the variables of interest in the circuit specification. A second drawback is that the abstraction that is built and used for each model-checking step may include portions that are useful in only a few of the model checking steps. Therefore needless extra computations are potentially performed, resulting in little benefit to the circuit verification.
Some methods have attempted to improve upon COI reduction by starting from a small portion of the dependency closure and extending the portion only when model checking fails to produce a satisfactory result. But these techniques also perform unnecessary computations on portions that are not relevant to the particular model-checking step being performed.
One method called the bounded cone of influence (BCOI) was proposed by A. Biere et al for symbolic model checking without BDDs [A. Biere, E. Clark, R. Raimi, and Y. Zhu; Verifying safety properties of a PowerPC™ microprocessor using symbolic model checking without BDDs; CAV'99; 1999]. However, even the BCOI method potentially includes irrelevant variables in the abstraction it builds, and the technique is not applicable to improve the widely used BDD-based approaches.


REFERENCES:
patent: 5119318 (1992-06-01), Paradies et al.
patent: 5469367 (1995-11-01), Puri et al.
patent: 5481717 (1996-01-01), Gaboury
patent: 5491639 (1996-02-01), Filkorn
patent: 5594656 (1997-01-01), Tamisier
patent: 5691925 (1997-11-01), Hardin et al.
patent: 5754454 (1998-05-01), Pixley et al.
patent: 5768498 (1998-06-01), Boigelot et al.
patent: 5905977 (1999-05-01), Goubault
patent: 5937183 (1999-08-01), Ashar et al.
patent: 6026222 (2000-02-01), Gupta et al.
patent: 6035109 (2000-03-01), Ashar et al.
patent: 6086626 (2000-07-01), Jain et al.
patent: 6131078 (2000-10-01), Plaisted
patent: 6148436 (2000-11-01), Wohl
patent: 6185516 (2001-02-01), Hardin et al.
patent: 6209120 (2001-03-01), Kurshan et al.
patent: 6247165 (2001-06-01), Wohl et al.
patent: 6292916 (2001-09-01), Abramovici et al.
patent: 6301687 (2001-10-01), Jain et al.
patent: 6308299 (2001-10-01), Burch et al.
patent: 6321186 (2001-11-01), Yuan et al.
patent: 6339837 (2002-01-01), Li
patent: 6341367 (2002-01-01), Downing
Hojati et al.,“Early Quantification and Partitioned Transition Relations”, Oct. 1996, Proceedings, IEEE International Conference on Computer Design: VLSI Computers and Processors. pp. 12-19.*
Bradley et al., “Compositional BDD Construction: A Lazy Algorithm”, Apr. 1998, Dept of Computer Science, University of Bristo pp. 1-8.*
Burch et al.,“Representing Circuits More Efficiently in Symbolic Model Checking”, 1991, 28thACM/IEEE Design Automation Conference, pp. 403-407.*
Campos, “Symbolic Model Checking in Practice”, Oct. 1999, IEEE Proceddings, XII Symposium on Integrated Circuits and System Design, pp. 98-101.*
Burch et al., “Symbolic Model Checking for Sequential Circuit Verification”, Apr. 1994, IEEE Transactions on Computer-Aided Design for Integrated Circuits and Systems, pp. 401-424.*
Zhang, “An Approach to Hierarchy Model Checking via Evaluating CTL Hierarchically”, Nov., 1995, IEEE Proceedings of the Fourth Asis Test Symposium, pp. 45-49.*
Berezin, S. et al, “A Compositional Proof System for the Modal &mgr;-Calculus and CCS,”Technical Report CMU-CS-97-105, Carnegie Mellon University, Jan. 15, 1997.
Berezin, S. et al, “Model Checking Algorithms for the &mgr;-Calculus,”Technical Report CMU-CS-96-180, Carnegie Mellon University, Sep. 23, 1996.
Bryant, R. E. et al, “Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation,”28thACM/IEEE Design Automation Conference, Paper 24.2, 1991, pp. 397-402.
Bryant, R. E., “Binary Decision Diagrams & Beyond,” Tutorial at ICCAD '95,Carnegie Mellon University, 1995.
Burch, J. R. et al, “Representing Circuits More Efficiently in Symbolic Model Checking,”28thACM/IEEE Design Automation Conference, Paper 24.3, 1991, pp. 403-407.
Burch, J. R. et al, “Sequential Circuit Verification Using Symbolic Model Checking,”27thACM/IEEE Design Automation Conference, Paper 3.2, 1990, pp. 46-51.
Campos, S., “Real-Time Symbolic Model Checking for Discrete Time Models,”Technical Report CMU-CS-94-146, Carnegie Mellon University, Pittsburgh, PA, May 2, 1994.
Chan, W. et al, Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-linear Constraints,Computer Aided Verification, 9thInternational Conference, CAV '97 Proceedings(O. Grumberg, Editor), Lecture Notes in Computer Science 1254, pp. 316-327, Haifa, Israel, Jun. 1997. Springer-Verlag (Revised in Dec. '98).
Chen, Y. et al, “PBHD: An Efficient Graph Representation for Floating Point Circuit Verification,”Technical Report CMU-CS-97-134, Carnegie Mellon University, May 1997.
Cheung, S. et al, “Checking Safety Properties Using Compositional Reachability Analysis,”ACM Transactions on Software Engineering and Methodology, vol. 8, No. 1, Jan. 1999, pp. 49-78.
Chiodo, M. et al, “Automatic Compositional Minimization in CTL Model Checking,”Proceedings of 1992 IEEE/ACM International Conference on Computer-Aided Design, Nov., 1992, pp. 172-178.
Chou, C., “The Mathematical Foundation of Symbolic Trajectory Evaluation,”International Conference on Computer-Aided Verification(CAV'99), Trento, Italy, Jul. 1999 pp. 196-207, Proceedings of CAV'99, Lecture Notes in Computer Science #1633 (Editors: Nicolas Halbwachs & Doron Peled), Springer-Verlog, 1999.
Clarke, E. et al, “Another Look at LTL Model Checking,”Technical Report CMU-CS-94-114, Carnegie Mellon University, Feb. 23, 1994.
Clarke, E. et al, “Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan,”Technical Report CMU-CS-94-103, Carnegie Mellon University, Jan. 1994.
Clarke, E. M. et al, “Formal Methods: State of the Art and Future Directions,”ACM Computing Surveys, vol. 28, No. 4, Dec. 1996, pp. 626-643
Clarke, E. M. et al, “Model Checking and Abstraction,”Proceedings

Affiliated with

Also associated with

Rating

Lazy symbolic model checking does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Lazy symbolic model checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Lazy symbolic model checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3186745