This Article 
 Bibliographic References 
 Add to: 
On Variable Ordering and Decomposition Type Choice in OKFDDs
December 1998 (vol. 47 no. 12)
pp. 1398-1403

Abstract—We present methods for the construction of small Ordered Kronecker Functional Decision Diagrams (OKFDDs). OKFDDs are a generalization of Ordered Binary Decision Diagrams (OBDDs) and Ordered Functional Decision Diagrams (OFDDs) as well. Starting with an upper bound for the size of an OKFDD representing a tree-like circuit, we develop different heuristics to find good variable orderings and decomposition types for OKFDDs representing two-level and multilevel circuits, respectively. Experimental results are presented to show the efficiency of our approaches.

[1] D.P. Appenzeller and A. Kuehlmann, “Formal Verification of a PowerPC Microprocessor,” Proc. Int'l Conf. Computer-Aided Design (ICCAD), pp. 79-84, San Jose, Calif., Nov. 1995.
[2] B. Becker, R. Drechsler, and M. Theobald, "OKFDDs versus OBDDs and OFDDs," Proc. Int'l Colloquium Automata, Languages, and Programming, pp. 475-486, 1995.
[3] 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.
[4] R.K. Brayton, G.D. Hachtel, C.T. McMullen, and A.L. Sangiovanni-Vincintelli, Logic Minimization Algorithms for VLSI Synthesis.Boston: Kluwer Academic, 1984.
[5] F. Brglez, D. Bryan, and K. Kozminski, "Combinatorial Profiles of Sequential Benchmark Circuits," Proc. IEEE Int'l. Symp. Circuits and Systems, IEEE Computer Soc. Press, Los Alamitos, Calif., 1989, pp. 1929-1934.
[6] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[7] 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.
[8] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[9] K.M. Butler and M.R. Mercer, Assessing Fault Model and Test Quality. Kluwer Academic, 1992.
[10] R. Drechsler and B. Becker, "Dynamic Minimization of OKFDDs," Proc. Int'l Conf. Computer Design, pp. 602-607, 1995.
[11] R. Drechsler and B. Becker, "PUMA: An OKFDD-Package and Its Implementation," Univ. Booth at European Design and Test Conf., 1995.
[12] 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.
[13] R. Drechsler, M. Theobald, and B. Becker, "Fast OFDD Based Minimization of Fixed Polarity Reed-Muller Expressions," Proc. European Design Automation Conf., pp. 2-7, 1994.
[14] M. Fujita, Y. Matsunaga, and T. Kakuda, “Interleaving Based Variable Ordering Methods for Ordered Binary Decision Diagrams,” Proc. Int'l Conf. Computer-Aided Design, pp. 38-41, 1993.
[15] M. Fujita, H. Fujisawa, and Y. Matsunaga, "Variable Ordering Algorithms for Binary Decision Diagrams and Their Evolution," IEEE Trans. Computer-Aided Design, vol. 12, pp. 6-12, 1993.
[16] 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.
[17] U. Kebschull, E. Schubert, and W. Rosenstiel, Multilevel Logic Synthesis Based on Functional Decision Diagrams Proc. European Conf. Design Automation, pp. 43-47, 1992.
[18] S. Malik, A.R. Wang, R.K. Brayton, and A. Sangiovanni-Vincentelli, Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment Proc. IEEE Int'l Conf. Computer-Aided Design (ICCAD-88), pp. 6-9, 1988.
[19] R. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," Proc. ICCAD-93, pp. 42-47, 1993.
[20] E. Schubert, U. Kebschull, and W. Rosenstiel, "Some Optimizations for Functional Decision Diagrams," Proc. IFIP WG 10.5 Workshop Applications of the Reed-Muller Expansion in Circuit Design, pp. 176-180,Hamburg, Germany, 1993.
[21] C. Tsai and M. Marek-Sadowska,"Boolean matching using generalized Reed-Muller forms," Proc. 31st ACM/IEEE Design Automation Conf., pp. 339-344, June 1994.
[22] I. Wegener, "Comments on 'A Characterization of Binary Decision Diagrams'," IEEE Trans. Computers, vol. 43, pp. 383-384, 1994.

Index Terms:
Decision diagrams, OKFDDs, variable ordering, tree-like circuits.
Rolf Drechsler, Bernd Becker, Andrea Jahnke, "On Variable Ordering and Decomposition Type Choice in OKFDDs," IEEE Transactions on Computers, vol. 47, no. 12, pp. 1398-1403, Dec. 1998, doi:10.1109/12.737685
Usage of this product signifies your acceptance of the Terms of Use.