This Article 
 Bibliographic References 
 Add to: 
Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions
November 1997 (vol. 46 no. 11)
pp. 1230-1245

Abstract—A new Boolean function representation scheme, the Indexed Binary Decision Diagram (IBDD), is proposed to provide a compact representation for functions whose Ordered Binary Decision Diagram (OBDD) representation is intractably large. We explain properties of IBDDs and present algorithms for constructing IBDDs from a given circuit. Practical and effective algorithms for satisfiability testing and equivalence checking of IBDDs, as well as their implementation results, are also presented. The results show that many functions, such as multipliers and the hidden-weighted-bit function, whose analysis is intractable using OBDDs, can be efficiently accomplished using IBDDs. We report efficient verification of Booth multipliers, as well as a practical strategy for polynomial time verification of some classes of unsigned array multipliers.

[1] P. Ashar, A. Ghosh, and S. Devadas, "Boolean Satisfiability and Equivalence Checking Using General Binary Decision Diagrams," Proc. Int'l Conf. Computer Design, pp. 259-264, 1991.
[2] J. Bitner, J. Jain, M. Abadir, J.A. Abraham, and D.S. Fussell, "Efficient Verification of Multiplier and Other Difficult Functions Using IBDDs," Proc. Custom Integrated Circuits Conf., pp. 5.5.1-5.5.5, 1992.
[3] J. Bitner, J. Jain, D.S. Fussell, J.A. Abraham, and M. Abadir, "Using Indexed BDDs in Specifying and Verifying Complex Circuits," Proc. IFIP Workshop Architecture and Logic Synthesis, 1993.
[4] B. Bollig, M. Sauerhoff, D. Sieling, and I. Wegener, "Read k Times Ordered Binary Decision Diagrams—Efficient Algorithms in Presence of Null Chains," Technical Report 474, Univ. of Dortmund, 1993.
[5] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[6] R.E. Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication," IEEE Trans. Computers, vol. 40, no. 2, pp. 206-213, Feb. 1991.
[7] R.E. Bryant and Y. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams," Proc. 32nd Design Automation Conf., pp. 535-541, 1995.
[8] J.R. Burch, "Multiplier Verification Using BDDs," Proc. 28th Design Automation Conf., pp. 408-412, 1991.
[9] E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang, "Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping," Proc. 30th Design Automation Conf., pp. 54-60, 1993.
[10] E.M. Clarke, M. Fujita, and X. Zhao, "Hybrid Decision Diagrams: Overcoming the Limitations of MTBDDs and BMDs," Proc. Int'l Conf. Computer-Aided Design, pp. 159-163, 1995.
[11] L. Fortune, J. Hopcroft, and E.-M. Schmidt, "The Complexity of Equivalence and Containment for Free Single Variable Program Schemes," Goos, Hartmanis, Ausiello, and Bohm, eds., Lecture Notes in Computer Science 62, pp. 227-240. Springer-Verlag, 1978.
[12] S.J. Friedman, "Efficient Data Structures for Boolean Function Representation," PhD dissertation, Computer Science Dept., Princeton Univ., 1990.
[13] K. Hwang,Computer Arithmetic, Principles, Architecture, and Design.New York: John Wiley&Sons, 1979.
[14] J. Jain, M. Abadir, J. Bitner, D.S. Fussell, and J.A. Abraham, "IBDDs: An Efficient Functional Representation for Digital Circuits," Proc. European Design Automation Conf., 1992.
[15] J. Jain, J. Bitner, D.S. Fussell, and J.A. Abraham, "Functional Partitioning for Verification and Related Problems," Proc. Brown/MIT VLSI Conf., pp. 210-226, 1992.
[16] J. Jain, J. Bitner, D.S. Fussell, and J.A. Abraham, "Probabilistic Verification of Boolean Functions," Formal Methods in System Design, vol. 1, pp. 61-115, July 1992.
[17] S.-W. Jeong, B. Plessier, G. Hachtel, and F. Somenzi, "Stuctural BDDs: Trading Canonicity for Structure in Verification Algorithms," Proc. Int'l Conf. Computer-Aided Design, pp. 464-467, 1991.
[18] T. Yamada and H. Yasuura, "On the Computational Power of Binary Decision Diagrams with Redundant Variables," Formal Methods in System Design, vol. 8, pp. 65-89, Jan. 1996.

Index Terms:
Boolean functions, BDDs, canonical representations, free BDDs, graph representations, IBDDs, OBDDs, satisfiability, verification.
Jawahar Jain, James Bitner, Magdy S. Abadir, Jacob A. Abraham, Donald S. Fussell, "Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions," IEEE Transactions on Computers, vol. 46, no. 11, pp. 1230-1245, Nov. 1997, doi:10.1109/12.644298
Usage of this product signifies your acceptance of the Terms of Use.