
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Laura HeinrichLitan, Paul Molitor, "Least Upper Bounds for the Size of OBDDs Using Symmetry Properties," IEEE Transactions on Computers, vol. 49, no. 4, pp. 360368, April, 2000.  
BibTex  x  
@article{ 10.1109/12.844348, author = {Laura HeinrichLitan and Paul Molitor}, title = {Least Upper Bounds for the Size of OBDDs Using Symmetry Properties}, journal ={IEEE Transactions on Computers}, volume = {49}, number = {4}, issn = {00189340}, year = {2000}, pages = {360368}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.844348}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Least Upper Bounds for the Size of OBDDs Using Symmetry Properties IS  4 SN  00189340 SP360 EP368 EPD  360368 A1  Laura HeinrichLitan, A1  Paul Molitor, PY  2000 KW  Binary decision diagrams KW  variable ordering KW  upper worst case bounds KW  partial symmetric Boolean functions. VL  49 JA  IEEE Transactions on Computers ER   
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. 509516, June 1978.
[2] C.l. Berge, Graphs. NorthHolland: Math. Library, 1991.
[3] R.E. Bryant, "GraphBased Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C35, No. 8, Aug. 1986, pp. 667690.
[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. ComputerAided Design of Integrated Circuits, vol. 13, no. 4, pp. 401424, Apr. 1994.
[5] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered BinaryDecision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293318, 1992.
[6] D.I. Cheng and M. Sadowska, "Verifying Equivalence of Functions with Unknown Input Correspondence," Proc. EDAC, pp. 8185, Feb. 1993.
[7] G. De Micheli, Synthesis and Optimization of Digital Circuits. McGrawHill, 1994.
[8] R. Drechsler and B. Becker, “Sympathy: Fast Exact Minimization of Fixed Polarity ReedMuller Expressions for Symmetric Functions,” Proc. European Conf. Design Automation, pp. 9197, 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. 985997, Nov. 1978.
[11] E. Felt, G. York, R. Brayton, and A. SangiovanniVincentelli, “Dynamic Variable Reordering for BDD Minimization,” Proc. European Conf. Design Automation, pp. 130135, 1993.
[12] M. Fujita, Y. Matsunaga, and T. Kakuda, "On variable Ordering of Binary Decision Diagrams for the Application of MultiLevel Logic Synthesis," Proc. European Design Automation Conf., pp. 5054, 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. 191195, 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. HeinrichLitan, “Least Upper Bounds on the Sizes of Symmetric Variable Order Based OBDDs,” master's thesis, Halle Univ., Inst. of Computer Science, D06099 Halle, Germany, 1997, Available via Internethttp://inferno.informatik.unihalle.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. 173180, 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. 472475, 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. ComputerAided Design, vol. 10, no. 4, pp. 436446, 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. 985999, 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. 126129, 1996.
[26] F. Mailhot and G.D. Micheli, “Technology Mapping Using Boolean Matching and Don't Care Sets,” Proc. European Conf. Design Automation, pp. 212216, 1990.
[27] C. Meinel and A. Slobodova, “Speeding Up Variable Reordering of OBDDs,” Proc. IEEE Int'l Conf. Computer Design, pp. 338343, 1997.
[28] J. Mohnke and S. Malik, “Permutation and Phase Independent Boolean Comparison,” INTEGRATION, the VLSI J., vol. 16, pp. 109129, 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. 459464, 1995.
[30] B.M.E. Moret,“Decision trees and diagrams,” Computing Surveys, vol. 14, no. 4, pp. 593623, 1982.
[31] S. Panda and F. Somenzi, “Who Are the Variables in Your Neigborhood,” Proc. IEEE Int'l Conf. ComputerAided Design, pp. 7477, 1995.
[32] S. Panda, F. Somenzi, and B. Plessier, "Symmetry Detection and Dynamic Variable Ordering of Decision Diagrams," Proc. ICCAD94, pp. 628631, 1994.
[33] R. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," Proc. ICCAD93, pp. 4247, 1993.
[34] C. Scholl, D. Möller, P. Molitor, and R. Drechsler, “BDD Minimization Using Symmetries,” IEEE Trans. ComputerAided Design, vol. 18, no. 2, pp. 81100, 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. 189196, 1996.
[36] T. van AardenneEhrenfest and N.G. de Bruijn, “Circuits and Trees in Oriented Linear Graphs,” Simon Stevin, vol. 28, pp. 203217, 1951.
[37] I. Wegener, “Optimal Decision Trees and OneTimeOnly Branching Programs for Symmetric Boolean Functions,” Information and Control, vol. 62, pp. 129143, 1984.