This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Least Upper Bounds for the Size of OBDDs Using Symmetry Properties
April 2000 (vol. 49 no. 4)
pp. 360-368

Abstract—This paper investigates reduced ordered binary decision diagrams (OBDD) of partially symmetric Boolean functions when using variable orders where symmetric variables are adjacent. We prove upper bounds for the size of such symmetry ordered OBDDs (SymOBDD). They generalize the upper bounds for the size of OBDDs of totally symmetric Boolean functions and nonsymmetric Boolean functions proven by Heap and Mercer [14], [15] and Wegener [37]. Experimental results based on these upper bounds show that the nontrivial symmetry sets of a Boolean function should be located either right up at the beginning or right up at the end of the variable order in order to obtain best upper bounds.

[1] S.B. Akers, “Binary Decision Diagrams,” IEEE Trans. Computers, vol. 27, no. 6, pp. 509-516, June 1978.
[2] C.l. Berge, Graphs. NorthHolland: Math. Library, 1991.
[3] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[4] J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill, "Symbolic Model Checking for Sequential Circuit Verification," IEEE Trans. Computer-Aided Design of Integrated Circuits, vol. 13, no. 4, pp. 401-424, Apr. 1994.
[5] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[6] D.I. Cheng and M. Sadowska, "Verifying Equivalence of Functions with Unknown Input Correspondence," Proc. EDAC, pp. 81-85, Feb. 1993.
[7] G. De Micheli, Synthesis and Optimization of Digital Circuits. McGraw-Hill, 1994.
[8] R. Drechsler and B. Becker, “Sympathy: Fast Exact Minimization of Fixed Polarity Reed-Muller Expressions for Symmetric Functions,” Proc. European Conf. Design Automation, pp. 91-97, 1995.
[9] R. Drechsler and B. Becker, Binary Decision Diagrams—Theory and Implementation, Kluwer Academic, 1998.
[10] C.R. Edwards and S.L. Hurst, “A Digital Synthesis Procedure under Function Symmetries and Mapping Methods,” IEEE Trans. Computers, vol. 27, no. 11, pp. 985-997, Nov. 1978.
[11] E. Felt, G. York, R. Brayton, and A. Sangiovanni-Vincentelli, “Dynamic Variable Reordering for BDD Minimization,” Proc. European Conf. Design Automation, pp. 130-135, 1993.
[12] M. Fujita, Y. Matsunaga, and T. Kakuda, "On variable Ordering of Binary Decision Diagrams for the Application of Multi-Level Logic Synthesis," Proc. European Design Automation Conf., pp. 50-54, 1991.
[13] G. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms. Kluwer Academic, 1996.
[14] M. Heap, "On the Exact Ordered Binary Decision Diagram Size of Totally Symmetric Functions," J. Electronic Testing: Theory, Application, vol. 4, no. 2, pp. 191-195, May 1993.
[15] M.A. Heap and M.R. Mercer, "Least Upper Bounds on OBDD Sizes," IEEE Trans. Computers, vol. 43, no. 6, June 1994.
[16] S.-Y. Huang and K.-T. Cheng, Formal Equivalence Checking and Design Debugging. Kluwer Academic, 1998.
[17] L. Heinrich-Litan, “Least Upper Bounds on the Sizes of Symmetric Variable Order Based OBDDs,” master's thesis, Halle Univ., Inst. of Computer Science, D-06099 Halle, Germany, 1997, Available via Internethttp://inferno.informatik.uni-halle.de/~molitor/ CDROM1999/monographienindex.html .
[18] S.L. Hurst, “Detection of Symmetries in Combinatorial Functions by Spectral Means,” IEE Electronic Circuits and Systems, vol. 1, no. 5, pp. 173-180, 1977.
[19] N. Ishiura, H. Sawada, and S. Yajima, "Minimization of Binary Decision Diagrams Based on Exchanges of Variables," Proc. IEEE Int'l Conf. Computer Aided Design, pp. 472-475, 1991.
[20] S.-W. Jeong, T.-S. Kim, and F. Somenzi, “An Efficient Method for Optimal BDD Ordering Computation,” Proc. Int'l Conf. VLSI and CAD, 1993.
[21] B.G. Kim and D.L. Dietmeyer, "Multilevel Logic Synthesis of Symmetric Switching Functions," IEEE Trans. Computer-Aided Design, vol. 10, no. 4, pp. 436-446, 1991.
[22] D.E. Knuth, The Art of Computer Programming, vol. 1,Addison Wesley, second ed. 1973.
[23] R.J. Bayardo, “Efficiently Mining Long Patterns From Databases,” ACM SIGMOD Conf. Management of Data, June 1998.
[24] C.Y. Lee, “Representation of Switching Circuits by Binary Decision Diagrams,” Bell System Technical J., vol. 38, pp. 985-999, 1959.
[25] L. Litan, P. Molitor, and D. Möller, “Least Upper Bounds on the Sizes of Symmetric Variable Order Based OBDDs,” Proc. Great Lakes Symp. VLSI, pp. 126-129, 1996.
[26] F. Mailhot and G.D. Micheli, “Technology Mapping Using Boolean Matching and Don't Care Sets,” Proc. European Conf. Design Automation, pp. 212-216, 1990.
[27] C. Meinel and A. Slobodova, “Speeding Up Variable Reordering of OBDDs,” Proc. IEEE Int'l Conf. Computer Design, pp. 338-343, 1997.
[28] J. Mohnke and S. Malik, “Permutation and Phase Independent Boolean Comparison,” INTEGRATION, the VLSI J., vol. 16, pp. 109-129, 1993.
[29] J. Mohnke, P. Molitor, and S. Malik, “Limits of Using Signatures for Permutation Independent Boolean Comparison,” Proc. Asia and South Pacific Design Automation Conf., pp. 459-464, 1995.
[30] B.M.E. Moret,“Decision trees and diagrams,” Computing Surveys, vol. 14, no. 4, pp. 593-623, 1982.
[31] S. Panda and F. Somenzi, “Who Are the Variables in Your Neigborhood,” Proc. IEEE Int'l Conf. Computer-Aided Design, pp. 74-77, 1995.
[32] S. Panda, F. Somenzi, and B. Plessier, "Symmetry Detection and Dynamic Variable Ordering of Decision Diagrams," Proc. ICCAD94, pp. 628-631, 1994.
[33] R. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," Proc. ICCAD-93, pp. 42-47, 1993.
[34] C. Scholl, D. Möller, P. Molitor, and R. Drechsler, “BDD Minimization Using Symmetries,” IEEE Trans. Computer-Aided Design, vol. 18, no. 2, pp. 81-100, 1999.
[35] D. Sieling, “Variable Orderings and the Size of OBDDs for Partially Symmetric Boolean Functions,” Proc. Synthesis and System Integration of Mixed Technologies, pp. 189-196, 1996.
[36] T. van Aardenne-Ehrenfest and N.G. de Bruijn, “Circuits and Trees in Oriented Linear Graphs,” Simon Stevin, vol. 28, pp. 203-217, 1951.
[37] I. Wegener, “Optimal Decision Trees and One-Time-Only Branching Programs for Symmetric Boolean Functions,” Information and Control, vol. 62, pp. 129-143, 1984.

Index Terms:
Binary decision diagrams, variable ordering, upper worst case bounds, partial symmetric Boolean functions.
Citation:
Laura Heinrich-Litan, Paul Molitor, "Least Upper Bounds for the Size of OBDDs Using Symmetry Properties," IEEE Transactions on Computers, vol. 49, no. 4, pp. 360-368, April 2000, doi:10.1109/12.844348
Usage of this product signifies your acceptance of the Terms of Use.