This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Efficient Minimization and Manipulation of Linearly Transformed Binary Decision Diagrams
September 2003 (vol. 52 no. 9)
pp. 1196-1209

Abstract—Binary Decision Diagrams are widely used in many applications in VLSI CAD. Linear transformations are one way to increase the computational power of BDDs. In this paper, we study linearly transformed BDDs (LTBDDs) from a practical point of view. First, we describe minimization techniques for LTBDDs. Then, we present efficient manipulation algorithms for LTBDDs. We give a large set of experimental results to demonstrate the efficiency of the algorithms.

[1] R.E. Bryant, Binary Decision Diagrams and Beyond: Enabeling Techniques for Formal Verification Proc. Int'l Conf. Computer Automated Design, pp. 236-243, 1995.
[2] A. Kuehlmann and F. Krohm, Equivalence Checking Using Cuts and Heaps Proc. Design Automation Conf., pp. 263-268, 1997.
[3] K. Yano, Y. Sasaki, K. Rikino, and K. Seki, Top-Down Pass-Transistor Logic Design IEEE J. Solid-State Circuits, vol. 31, no. 6, pp. 792-803, 1996.
[4] P. Buch, A. Narayan, A.R. Newton, and A.L. Sangiovanni-Vincentelli, Logic Synthesis for Large Pass Transistor Circuits Proc. Int'l Conf. Computer Automated Design, pp. 663-670, 1997.
[5] R. Drechsler and W. Günther, Towards One-Pass Synthesis. Kluwer Academic Publishers, 2002.
[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] U. Kebschull, E. Schubert, and W. Rosenstiel, Multilevel Logic Synthesis Based on Functional Decision Diagrams Proc. European Conf. Design Automation, pp. 43-47, 1992.
[8] R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M.A. Perkowski, Efficient Representation and Manipulation of Switching Functions Based on Ordered Kronecker Functional Decision Diagrams Proc. Design Automation Conf., pp. 415-419, 1994.
[9] B. Becker, R. Drechsler, and R. Werchner, On the Relation between BDDs and FDDs Information and Computation, vol. 123, no. 2, pp. 185-197, 1995.
[10] J. Gergov and C. Meinel, Efficient Analysis and Manipulation of OBDDs Can Be Extended to FBDDs IEEE Trans. Computers, vol. 43, pp. 1197-1209, 1994.
[11] D. Sieling and I. Wegener, Graph Driven BDDs A New Data Structure for Boolean Functions Theoretical Computer Science, vol. 141, pp. 283-310, 1995.
[12] J. Bern, C. Meinel, and A. Slobodová, Some Heuristics for Generating Tree-Like FBDD Types IEEE Trans. Computer Automated Design, vol. 15, pp. 127-130, 1996.
[13] D. Sieling, The Complexity of Minimizing FBDDs Proc. Symp. Math. Foundations of Computer Science, Springer Verlag, pp. 251-261, 1999.
[14] W. Günther and R. Drechsler, Minimization of Free BDDs Proc. ASP Design Automation Conf., pp. 323-326, 1999.
[15] W. Günther, Minimization of Free BDDs Using Evolutionary Techniques Proc. Int'l Workshop Logic Synthesis, pp. 167-172, 2000.
[16] R.E. Bryant and Y. Chen, "Verification of Arithmetic Functions with Binary Moment Diagrams," Proc. 32nd Design Automation Conf., pp. 535-541, 1995.
[17] B. Becker, R. Drechsler, and R. Enders, On the Computational Power of Bit-Level and Word-Level Decision Diagrams Proc. ASP Design Automation Conf., pp. 461-467, 1997.
[18] W. Günther and R. Drechsler, On the Computational Power of Linearly Transformed BDDs Information Processing Letters, vol. 75, no. 3, pp. 119-125, 2000.
[19] C. Meinel, F. Somenzi, and T. Theobald, Linear Sifting of Decision Diagrams and Its Application in Synthesis IEEE Trans. Computer Automated Design, vol. 19, no. 5, pp. 521-533, 2000.
[20] R. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," Proc. ICCAD-93, pp. 42-47, 1993.
[21] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[22] R. Drechsler and B. Becker, Binary Decision Diagrams Theory and Implementation. Kluwer Academic, 1998.
[23] K.S. Brace, R.L. Rudell, and R.E. Bryant, Efficient Implementation of a BDD Package Proc. Design Automation Conf., pp. 40-45, 1990.
[24] C. Meinel and T. Theobald, Local Encoding Transformations for Optimizing OBDD-Representations of Finite State Machines Proc. Int'l Conf. Formal Methods in Computer Automated Design, pp. 404-418, 1996.
[25] F. Somenzi, CUDD: CU Decision Diagram Package Release 2.3.0. Univ. of Colorado at Boulder, 1998.
[26] S. Minato, N. Ishiura, and S. Yajima, Shared Binary Decision Diagrams with Attributed Edges for Efficient Boolean Function Manipulation Proc. Design Automation Conf., pp. 52-57, 1990.
[27] S.J. Friedman and K.J. Supowit, Finding the Optimal Variable Ordering for Binary Decision Diagrams Proc. Design Automation Conf., pp. 348-356, 1987.
[28] R. Drechsler, N. Drechsler, and W. Günther, Fast Exact Minimization of BDDs IEEE Trans. Computer Automated Design, vol. 19, no. 3, pp. 384-389, 2000.
[29] R. Drechsler, Evolutionary Algorithms for VLSI CAD. Kluwer Academic, 1998.
[30] R. Drechsler, B. Becker, and N. Göckel, A Genetic Algorithm for Variable Ordering of OBDDs IEE Proc., vol. 143, no. 6, pp. 364-368, 1996.
[31] B. Becker, R. Drechsler, and R. Werchner, On the Relation between BDDs and FDDs LATIN, pp. 72-83, 1995.
[32] S. Yang, Logic Synthesis and Optimization Benchmarks User Guide Technical Report 1/95, Microelectronic Center of North Carolina, 1991.
[33] F. Brglez and H. Fujiwara, A Neutral Netlist of 10 Combinational Circuits and a Target Translator in Fortran Proc. Int'l Symp. Circuits and Systems, special session on ATPG and fault simulation, pp. 663-698, 1985.

Index Terms:
Binary decision diagram, linear transformation, minimization, formal verification.
Citation:
Wolfgang G?nther, Rolf Drechsler, "Efficient Minimization and Manipulation of Linearly Transformed Binary Decision Diagrams," IEEE Transactions on Computers, vol. 52, no. 9, pp. 1196-1209, Sept. 2003, doi:10.1109/TC.2003.1228514
Usage of this product signifies your acceptance of the Terms of Use.