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)