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

## No comments:

## Post a Comment

Your Comments... (comments are moderated)