Why Formal Verification?

Different simulation were under use way back in 1980s itself. These are used to check the functionality of the digital designs. Even after the enormous progress of the simulation methodologies, complexities involved in the simulation have not reduced. The high cost factor of the supporting simulation libraries and more time consumed in generating input patterns are the two main road blocks of simulation tools.

The existing general simulation methodologies are slow.

Consider two types of simulators:
- Event based and
- Cycle based simulators.

“Event based simulators” simulate whenever there is an event i.e. there is a change in data value. Modelsim simulator tool is a good example for this. Since they are waiting for event they are inherently slow.

On the other hand, “cycle based simulators” simulate every cycle. These types of simulators do not wait for event and simulate independently. Hence they are around 10 times faster event based simulators.

The other type of simulators like code compiled simulators and native compiled simulators convert HDL code to either C or machine level language directly. This is known as system level simulation. SystemC and System Verilog strongly came out as a possible solution to functional verification complexities. This couldn’t solve the complexities of the simulation process as these languages are sequential in nature unlike HDL languages which are concurrent in nature.

Despite of all these developments 70% of the time is utilized for design verification and validation and only 30% of time is spent on design development. Considering the time to market span of the industry, it is essential to reduce the verification time without compromising the quality of the design verification process. Formal Verification reduces the simulation time and complexities involved in it. It is desirable to have formal verification technique at system level [2] also. Several approaches are presented [2-7] which allow verification at system level also.

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