Recent Advances in SAT Based Formal Verification

SAT can be used for model checking and the method is known as Bounded Model Checking. Bounded Model Checking based on SAT methods was introduced by Biere et al. [7]. This is rapidly gaining popularity as a complementary technique to BDD-based symbolic model checking. A more compact CNF for the BMC problem is used to generate structural processing. This makes the resulting SAT problem easier for the SAT solver to solve. Traditional model checking uses a method, known as cone of influence (COI) reduction. An improvement on this method the method of bounded cone of influence (BCOI) reduction. Variable ordering has long been recognized as a key determinant of the performance of SAT solvers. BMC tools using circuit-based SAT solvers essentially use some variant of the J-frontier justification heuristic popularly used in sequential ATPG tools.

Several case studies mentioned in [7] which employed BMC as Formal Verification methodology has proven the capability of the model successfully. BMC was found to significantly outperform the BDD based Symbolic Model Verification model checker for several of the benchmarks. The case studies were carried out on processors like PowerPC and Intel Pentium 4. Thus it is generally accepted in the research and industrial community that SAT-BMC tools require minimal tuning effort and work particularly well on large designs where bugs need to be searched at shallow to medium depths.
The paper [7] further surveys the several other latest trends in Model Checking algorithm based on SAT solvers. Few of them are named here: SAT-based Unbounded Model Checking, ATPG-based Model Checking, Quantified Boolean Formulae (QBF).

The SAT-based verification has been emerged as an orthogonal technology to BDD-based model checking techniques (bounded and unbounded). SAT based techniques require fewer users tuning as well as less sensitive to the problem size. However, major challenge is to develop a verification methodology which employs both SAT and BDD methods in a manner best suited to utilize their respective strengths.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Hybrid Formal Verification Techniques
Formal Verification Example