This Article 
 Bibliographic References 
 Add to: 
Exact Minimization of Binary Decision Diagrams Using Implicit Techniques
November 1998 (vol. 47 no. 11)
pp. 1282-1296

Abstract—This paper addresses the problem of binary decision diagram (BDD) minimization in the presence of don't care sets. Specifically, given an incompletely specified function g and a fixed ordering of the variables, we propose an exact algorithm for selecting f such that f is a cover for g and the binary decision diagram for f is of minimum size. The approach described is the only known exact algorithm for this problem not based on the enumeration of the assignments to the points in the don't care set. We show also that our problem is NP-complete. We show that the BDD minimization problem can be formulated as a binate covering problem and solved using implicit enumeration techniques. In particular, we show that the minimum-sized binary decision diagram compatible with the specification can be found by solving a problem that is very similar to the problem of reducing incompletely specified finite state machines. We report experiments of an implicit implementation of our algorithm, by means of which a class of interesting examples was solved exactly. We compare it with existing heuristic algorithms to measure the quality of the latter.

[1] A. Blumer, A. Ehrenfeucht, D. Haussler, and M. Warmuth, "Occam's Razor," Information Processing Letters, vol. 24, NorthHolland, pp. 377-380, 1987.
[2] K.S. Brace, R.L. Rudell, and R.E. Bryant, Efficient Implementation of a BDD Package Proc. Design Automation Conf., pp. 40-45, 1990.
[3] R.K. Brayton, G.D. Hachtel, C.T. McMullen, and A.L. Sangiovanni-Vincintelli, Logic Minimization Algorithms for VLSI Synthesis.Boston: Kluwer Academic, 1984.
[4] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[5] S.-C. Chang, D.I. Cheng, and M. Marek-Sadowska, "Minimizing ROBDD Size of Incompletely Specified Multiple Output Functions," Proc. European Design and Test Conf., pp. 620-624, Mar. 1994.
[6] O. Coudert, C. Berthet, and J.C. Madre, "Verification of Sequential Machines Using Functional Boolean Vectors," Proc. IFIP Int'l Workshop, Applied Formal Methods for Correct VLSI Design, Nov. 1989.
[7] O. Coudert,C. Berthet,, and J.C. Madre,“Verification of synchronous sequential machines based on symbolic execution,” LNCS: Automatic Verification Methods for Finite State Systems, J. Sifakis, ed., vol. 407, Springer-Verlag, June 1989, pp. 365-373.
[8] A. Grasselli and F. Luccio, "A Method for Minimizing the Number of Internal States in Incompletely Specified Sequential Networks," IRE Trans. Electronic Computers, vol. 14, no. 3, pp. 350-359, June 1965.
[9] K. Hirata, S. Shimozono, and A. Shinoara, "On the Hardness of Approximating the Minimum Consistent OBDD Problem," Proc. Fifth Scandinavian Workshop Algorithm Theory, July 1996.
[10] T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli, "A Fully Implicit Algorithm for Exact State Minimization," Proc. Design Automation Conf., pp. 684-690, June 1994.
[11] T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli, Synthesis of FSMs: Functional Optimization. Kluwer Academic, 1997.
[12] L. Lavagno, P. McGeer, A. Saldanha, and A.L. Sangiovanni-Vincentelli, "Timed Shannon Circuits: A Power-Efficient Design Style and Synthesis Tool," Proc. 32nd Design Automation Conf., pp. 254-260, June 1995.
[13] A. Oliveira, L. Carloni, T. Villa, and A. Sangiovanni-Vincentelli, "Exact Minimization of Binary Decision Diagrams Using Implicit Techniques," Technical Report No. UCB/ERL M96/16, Apr. 1996.
[14] A.L. Oliveira, "Inductive Learning by Selection of Minimal Complexity Representations," PhD thesis, Univ. of California, Berkeley, Electronics Research Laboratory, College of Eng., Univ. of California, Berkeley, Dec. 1994. Memorandum No. UCB/ERL M94/97.
[15] R. Ranjan, T. Shiple, and R. Hojati, "Exact Minimization of BDDs Using Don't Cares," EE290ls Project Report, May 1993.
[16] M. Sauerhoff and I. Wegener, "On the Complexity of Minimizing the OBDD Size for Incompletely Specified Functions," Forschungsbericht Nr. 560, Universität Dortmund, 1994.
[17] T. Shiple, R. Hojati, A. Sangiovanni-Vincentelli, and R. Brayton, "Heuristic Minimization of BDDs Using Don't Cares," Proc. Design Automation Conf., pp. 225-231, June 1994.
[18] Y. Takenaga and S. Yajima, "NP-Completeness of Minimum Binary Decision Diagram Identification," Technical Report COMP 92-99, Inst. of Electronics, Information, and Comm. Engineers (of Japan), Mar. 1993.
[19] H. Touati, H. Savoj, B. Lin, R. Brayton, and A. Sangiovanni-Vincentelli, "Implicit State Enumeration of Finite State Machines Using BDDs," Proc. Int'l Conf. Computer-Aided Design, pp. 130-133, 1990.

Index Terms:
Binary decision diagrams, incompletely specified functions, minimization of logic functions, incompletely specified finite state machines, state minimization, implicit logic computations.
Arlindo L. Oliveira, Luca P. Carloni, Tiziano Villa, Alberto L. Sangiovanni-Vincentelli, "Exact Minimization of Binary Decision Diagrams Using Implicit Techniques," IEEE Transactions on Computers, vol. 47, no. 11, pp. 1282-1296, Nov. 1998, doi:10.1109/12.736442
Usage of this product signifies your acceptance of the Terms of Use.