Equivalence Checking (EC)

Here the goal is to ensure the equivalence of two given circuit descriptions. These circuit descriptions can be in different levels of abstractions. EC translate both designs to an internal format. In matching phase, it establishes correspondence between the two designs and proves the equivalence or in equivalence. It determines if two expressions, say F and G denote the same truth table. The extract representation of logic expressions F and G are verified either by satisfiability algorithms (propositional resolution) or by ROBDD. In the case of in-equivalence, a counter example is generated and debugging phase starts. Generated counter examples are not reachable during normal circuit operation. [2]

Combinational Equivalence Checking

Design is considered as purely combinational. Each state element is modeled as additional primary inputs and outputs. A BDD can be constructed by considering depth first vs. breadth first construction style for optimized use of memory by keeping only few levels in memory, rest on disk. Dynamic reordering can generate excessive memory usage. Partitioning of Boolean space, each represented by a separate BDD reduces complexities of verification process.

The available commercial tools which employ this methodology are: Design Verifier from Chrysalis, Formality from Synopsys, Affirma from Cadence and Tornado from Verysys.
Challenges of EC

* Complexity: It is well known fact that Moore’s law still rules! More the complexity of circuit BDDs suffer from “memory explosion” problem.

* Proof technology integration: BDDs and SAT are most popular methods applied in hardware verification tools. Modern verification tools make use of multiengine approach that combine different methodologies, like SAT, BDD and ATPG. The successful combination approach is still a bottleneck.

* Matching: For larger designs matching algorithms either fails or consume enormous computation time.

* Arithmetic: Often BDD and SAT have difficulties with arithmetic circuit, like multipliers. Arithmetic circuits that are concurrent in nature are a challenge to FV.

* Analog and mixed signal: Modern SOC designs have both analog and digital circuits integrated together. Present proof technologies assume that the circuit is purely digital; practically it is not the case. Verifying analog circuits is most challenging task.

* Multi clock domains: Present day EC solvers can’t work with multiple clock domains whereas most of the practical designs have more than one clock domain.

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)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques
Formal Verification Example