09 October 2007

Introduction to Formal Verification


Around 70% of the overall design time and cost is spent on verification and validation. It becomes very important to verify the correctness of the circuits. Modern complex designs contain several hundred million transistors. Verification of such a complex system in a shorter span of time becomes a dominating factor before it goes silicon level. Several Formal Verification methods have been proposed and are under research as an alternative to classical simulation techniques, since it can’t guarantee sufficient coverage of the design. In addition to this simulation is a slow process. Formal Verification (FV) techniques ensure 100% functional correctness and they are more reliable and cost effective, less time consuming. The main concept of FV is not to simulate some vectors, instead prove the functional correctness of a design.

There are different proof methodologies employed, the most common being Equivalence Checking (EC) methodology. The basic methodology used in most of the industry verification tools, known as Binary Decision Diagram (BDD) and Satisfiability (SAT) solvers, come under this category. These traditional methods fail to handle complex circuits efficiently. Hence new trends like SAT based Symbolic Model Checking are emerging which fall under Model Checking (MC) (Also known as Property Checking (PC)) methodology. New techniques like Bounded Model Checking (BMC) based on SAT solvers are promising better efficient methods of Formal Verification. Hybrid Formal Verification methods are under investigation which employs strength of respective Formal Verification models. Each of these methods has their own pros and cons which will be discussed in subsequent articles. The papers I have referred are listed below. For SAT solver related latest developments, [7] is referred and for hybrid Formal Verification methods [6] is referred.

Reference

[1] Sandeep K. Shukla, An Introduction to Formal Verification, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 3/4/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 SongFormal Verification Methods, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 5/4/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/, 13/4/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/, 13/4/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/, 13/4/07

Related Articles

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

Recent Advances in SAT Based Formal Verification

Hybrid Formal Verification Techniques

Formal Verification Example

No comments:

Post a Comment

Your Comments... (comments are moderated)