
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 12301245, November, 1997.  
BibTex  x  
@article{ 10.1109/12.644298, author = {Jawahar Jain and James Bitner and Magdy S. Abadir and Jacob A. Abraham and Donald S. Fussell}, title = {Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions}, journal ={IEEE Transactions on Computers}, volume = {46}, number = {11}, issn = {00189340}, year = {1997}, pages = {12301245}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.644298}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions IS  11 SN  00189340 SP1230 EP1245 EPD  12301245 A1  Jawahar Jain, A1  James Bitner, A1  Magdy S. Abadir, A1  Jacob A. Abraham, A1  Donald S. Fussell, PY  1997 KW  Boolean functions KW  BDDs KW  canonical representations KW  free BDDs KW  graph representations KW  IBDDs KW  OBDDs KW  satisfiability KW  verification. VL  46 JA  IEEE Transactions on Computers ER   
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 hiddenweightedbit 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. 259264, 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.15.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, "GraphBased Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C35, No. 8, Aug. 1986, pp. 667690.
[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. 206213, Feb. 1991.
[7] R.E. Bryant and Y. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams," Proc. 32nd Design Automation Conf., pp. 535541, 1995.
[8] J.R. Burch, "Multiplier Verification Using BDDs," Proc. 28th Design Automation Conf., pp. 408412, 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. 5460, 1993.
[10] E.M. Clarke, M. Fujita, and X. Zhao, "Hybrid Decision Diagrams: Overcoming the Limitations of MTBDDs and BMDs," Proc. Int'l Conf. ComputerAided Design, pp. 159163, 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. 227240. SpringerVerlag, 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. 210226, 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. 61115, 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. ComputerAided Design, pp. 464467, 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. 6589, Jan. 1996.