Binary Decision Diagram (BDD)

Decision to traverse in the binary tree is taken depending on the binary value of the variable. Each node of the diagram represent sets of objects (states) encoded as Boolean functions. Reduced Ordered BDD (ROBDD) is canonical and canonicity is essential for verification.

Certain rules have to be followed to construct ROBDD.

They are:

1. Terminal should not duplicate. Remove all duplicate terminals.
2. Remove all duplicate nodes.
3. Remove internal nodes with identical children.

Consider a function f = ac + bc. Binary Decision Diagram for this function is shown in Figure (1). Straight lines in the diagram shows path of the binary one and dotted line show binary zero. All possible combinations of variables a, b and c and corresponding outputs are drawn in the diagram. The binary values within the square boxes represent the possible output values for function f with different input combinations. This BDD can be reduced to obtain ROBDD.

Figure (1) Binary Decision Diagram (BDD) construction [1]

The steps to obtain a ROBDD are shown Figure (2).

Figure (2) ROBDDD construction [1]
Figure (3) Application to verification [1]

Application of these BDDs to check the equivalence of combinational circuits is depicted in Figure (3). If two functions, say, F= a’bc+ab’c and G=ac+bc are equivalent then their BDDs are identical. ROBDD for both F and G are identical as shown in Figure (3). Thus this methodology is applied in formal verification techniques to check the equivalence of circuit description. Some industrial packages that employ this methodology are: Intel, Lucent, Cadence, Synopsys (Formality), Bull Systems, etc.

There are some critical drawbacks related to BDD. For larger functions there may not be a canonical form existing or the existing one may be too large (exponential). Operations like complementation may yield a representation of exponential size. In this case equivalence and tautology checking becomes hard.

A detailed discussion over variable ordering, breadth first manipulation, node decompositions, partitioned ROBDDs, verification of arithmetic circuits etc can be found in [4].

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