Methodologies in Formal Verification

Mainly 3 methodologies are followed in Formal Verification of hardware designs.

They are:

1. Equivalence Checking (EC)
2. Model Checking (MC)
3. Theorem Proving (TP)

In Equivalence Checking method, Design Under Test and reference are reduced to an equation and Design Under Test is compared with reference design. This methodology is traditionally employed in most of the Formal Verification tools and well established as it is easy to implement.

The second Model Checking is comparatively complex and only academic tools are available. Here Design Under Test is verified for the satisfaction of given specification under all conditions. The specifications or properties provided are in terms of mathematical formulae or equations.

The third methodology, Theorem Proving is toughest of all but provides very accurate comparison and hence most efficient. Here theorem is extracted from Design Under Test and proved with respect to the reference design. Few of the industry level tools provide this methodology and it is of more research interest yet.

In each of these methodologies we can find sub methods which are employed to implement the Formal Verification algorithm. As we noted, Equivalence Checking is most commonly employed in traditional method. Under this category we find two important methodologies.

They are:

1. Binary Decision Diagram (BDD): This is more commonly implemented in Formal Verification tools. (E.g. Formality by Synopsys).

2. Satisfiability (SAT) Solvers: Several advancements are happening based on this method.

The Binary Decision Diagram and SAT solvers are fundamental methods used in latest FV developments like Symbolic Model Verification (SMV) and also Bounded Model Checking (BMC). Both the BDD and SAT solvers are professionally employed in several industrial Formal Verification tools. They are the basis of all advancement in Formal Verification. Hence it is very relevant to discuss about Binary Decision Diagram and SAT solvers in general.

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
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