13 October 2007

Concept of Formal Verification

In Formal Verification process Design Under Test (DUT) is compared with proven design or set of properties (or specifications). Proven design is considered as Reference design and is also called as Golden Reference. Both the DUT and reference is reduced to Boolean equations or mathematical theorem or models and these are compared to each other.

The DUT and reference design may be in different level of abstraction i.e. either it can be in RTL or gate level. DUT can be HDL (Verilog or VHDL or any other) code or Netlist. Similarly reference design can also be in HDL code or Netlist. Only prerequisite here is DUT and reference should have same functionality.

As shown in the figure code and post synthesis netlist can be formally verified. The post synthesis netlist is generated either in .lib or .v or .VITAL format. Formal Verification tools allow verifying these two netlists that represent same functionality.



Figure Showing Formal Verification Flow

The most attractive feature of any Formal Verification method is that the verification is completely exhaustive which not the case with simulations is. Consideration of “all possible cases” is implicit in formal verification. The correctness of circuit description is guaranteed mathematically, regardless the input values. There is no need to generate expected output sequences. The formal verification can generate an error trace if a property fails which can be confirmed by simulation. Formal verification is useful to detect and locate errors in designs.

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?

No comments:

Post a Comment

Your Comments... (comments are moderated)