Hybrid Formal Verification Techniques

Traditional formal techniques like Model Checking and Theorem Proving are capable of analyzing and finding all bugs in a design. However, they suffer from several drawbacks due to which their applicability in practice is restricted. Model checking is limited by well known state explosion problem. For the effective use of theorem proving technique, highly knowledge and skillful manpower is necessary. In this context hybrid techniques where both formal and informal techniques are used in conjunction with each other are gaining more popularity. The general goal of a hybrid technique is to enhance coverage of the state space traversed in order to address the verification bottleneck, by using the strengths of individual methods.

Hybrid Formal Verification approaches is classified into four categories.

They are:

1. Methods combining formal and informal techniques
2. Combination of two formal techniques
3. Combination of two informal techniques
4. Combination of multiple verification approaches

Symbolic Model Verification (SMV) is a powerful method for Formal Verification but most of the realistic designs are too large and complex for pure symbolic simulation techniques. A method surveyed by [6] used concept of synthesis and verification. This hybrid technique achieved better coverage and quicker in finding bugs. One more hybrid technique which combines model checking and test generation, used general graph theoretic model, functional fault model and test generation procedures. This method is highly suitable for pipelined processors.

It is interesting to note that a number of research activities are going on in hybridization of ATPG and formal techniques. ATPGs avoid state explosion problem while formal methods are “complete”. Hybridization of these two strengthens the verification. In one of the method surveyed in [6], formal specifications (or properties) are used as input to the test generator. This method was quite successful in dealing with commercial designs. Another method combined both ATPG and BDD with the SMV. As noted by [6] results showed better coverage than either symbolic techniques or simulation in isolation. Several other hybrid techniques which combine ATPG, BDD and SMV can be found in [6].

Effectively combining two formal methods like theorem proving and model checking is a great challenge to research community. The experiment that combined “Symbolic Trajectory Evolution” (STE) with theorem proving method showed good results for the verification of 64-bit integer multiplier. Some other theorem proving methods that use external tools like ORACLE for checking formulas as theorem during proof search and they use ORACLE interface to decide Boolean formulas through connections to BDD and SAT solving libraries.

Another tool, MIST, surveyed by [6] hybridizes two model checking techniques. The technique enables an interface between STE and SMC-BDD or SAT based solvers. In this technique, once the initial set of states is obtained by using STE, SMC is used to check the property on the original circuit model. Thus the model MIST enhances both the capacity and performance of SMC. The method helps the debugging process by letting the verifier focus on critical and error prone areas.

Various other methods combining informal methods are also emerging. One among them employs “computer learning” and “Bayesian Networks” and couple of others use model based randomized functional verification.

The first proposed method combining multiple verification approaches used test pattern generation, no-reachability analysis, symbolic simulation, SAT based BMC, symbolic fix point computation and automatic abstraction. These techniques helped to focus coverage issues much earlier in the design cycle, to expose bugs in deep circuit blocks.

Hybrid Formal Verification techniques are employed in commercial tools like Megellan, Formality by Synopsys; Incissive by Cadence; FormalPro by Mentor Graphics.

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
Formal Verification Example