ASIC-System on Chip-VLSI Design: Model Checking

In Model Checking property is in the form of a temporal logic formula and sequential properties are usually represented in temporal logic. Various variants of temporal logic formulae are available such as Linear Temporal Logic (LTL) or Computation Tree Logic (CTL). These logics usually require dedicated algorithms. The truth of formula is determined against a semantic model of the implementation. The system is modeled by Labeled Transition Graph (LTG, LTS, and Finite Kripke Structure). The algorithm carries an exhaustive search through the state space of the system to determine if the specified property holds or not. For larger designs, this search creates “state explosion” problem. Symbolic Model Checking comes as a partial solution this problem.

Figure (1) Model Checking [3]
Figure (2) Symbolic Model Checking [3]

Symbolic Model Checking

Here transition or output relations and sets of states are symbolically represented using ROBDD as shown in the Figure (2). Model checking used an explicit representation of states. A large Hash table is used to store individual states. The states reached during a depth first traversal of the state space are memorized as hash values. Since the number of states of even small systems can be very large, e.g., a 128 bit shift register has 2128 states; this method does not scale, in particular for sequential circuits. This problem is called state explosion problem. In symbolic model checking this problem is sorted out. Symbolic model checking operates on sets of states instead of individual states and represents sets of states symbolically in a compact form.

Advantages of MC

* The verification process is completely automated.
* Counter examples are generated for identifying design errors.

Disadvantages of MC

* The main drawback is State explosion problem because of which maximum of 400 Boolean variables can be processed. In complex designs data paths pose problems.

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