This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Characterization of Binary Decision Diagrams
February 1993 (vol. 42 no. 2)
pp. 129-137

Binary decision diagrams (BDDs) are a representation of Boolean functions. Its use in the synthesis, simulation, and testing of Boolean circuits has been proposed by various researchers. In all these applications of BDDs solutions to some fundamental computational problems are needed. A characterization of BDDs in terms of the complexity of these computational problems is presented. A tighter bound on the size of an ordered BDD that can be computed from a given Boolean circuit is presented. On the basis of the results, a case is made for exploring the use of repeated BDDs, with a small number of repeated variables, and free BDDs for some applications for which only ordered BDDs have been used so far.

[1] M. S. Abadir and H. K. Reghabati, "Functional test generation for digital circuits described using binary decision diagram,"IEEE Trans. Comput., vol. C-35, no. 4, pp. 375-379, Apr. 1986.
[2] A. V. Aho and J. D. Ullman,Principles of Compiler Design. Reading, MA: Addison-Wesley, 1979.
[3] S. B. Akers, "Binary decision diagrams,"IEEE Trans. Comput., vol. C- 27, no. 6, p. 509-516, June 1978.
[4] S. B. Akers, "Functional testing using binary decision diagrams," inProc. 8th Int. Symp. Fault Tolerant Comput., June 1978, pp. 82-92.
[5] S. B. Akers, "A procedure for functional design verification," inProc. IEEE/ ACM 10th Int. Fault Tolerant Comput. Symp., Oct. 1980, pp. 65-67.
[6] P. Ashar, S. Devadas, and K. Keutzer, "Testability properties of multi-level logic networks derived from binary decision diagrams," inProc. Santa Cruz Conf. Advanced Res. VLSI, Mar. 1991, pp. 35-54.
[7] C. L. Berman, "Ordered binary decision diagrams and circuit structure," inProc. ICCD, 1989, pp. 392-395.
[8] B. Bhattacharya and S.C. Seth, "On the reconvergent structure of combinational circuits with applications to compact testing," inProc. IEEE/ACM 17th Int. Fault-Tolerant Comput. Symp., 1987, pp. 264-269.
[9] M. Blum, A.K. Chandra, and M.N. Wegman, "Equivalence of free Boolean graphs can be decided probabilistically in polynomial time,"Inform. Processing Lett., vol. 10, no. 2, pp. 80-82, Mar. 1980.
[10] K. S. Brace, R. L. Rudell, and R. E. Bryant, "Efficient implementation of a BDD package," in27th ACM/IEEE Design Automat. Conf., 1990, pp. 40-45.
[11] R. E. Bryant, "Graph-based algorithms for Boolean function manipulation,"IEEE Trans. Comput., vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[12] R. E. Bryant, "Symbolic manipulation of Boolean functions using a graphical representation," inProc. 22nd IEEE/ACM Design Automat. Conf., June 1985, pp. 688-694.
[13] R. E. Bryant, "Symbolic verification of MOS circuits," inProc. 1985 Chapel Hill Conf. VLSI, Computer Science Press, pp. 419-438.
[14] R. E. Bryant, "On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication,"IEEE Trans. Comput., vol. C-40, no. 2, pp. 205-213, Feb. 1991.
[15] J. Burch, "Using BDDs to verify multipliers," inProc. 1991 Int. Workshop Formal Methods in VLSI Design, Jan. 1991.
[16] J.R. Burch et al., "Sequential Circuit Verification Using Symbolic Model Checking,"Proc. 27th Design Automation Conf., IEEE CS Press, 1990, pp. 46-51.
[17] S. Chakravarty and H. B. Hunt III, "On computing signal probability and detection probability for stuck-at faults,"IEEE Trans. Comput., vol. 39, no. 11, pp. 1369-1377, Nov. 1990.
[18] S. Chakravarty, "A testable multiplexer realization of CMOS combinational circuits," inProc. 1989 IEEE Int. Test Conf., pp. 509-518.
[19] E. Cerny and J. Gecsei, "Simulation of MOS circuits by decision diagrams,"IEEE Trans. Computer-Aided Design, vol. CAD-4, pp. 685-693, Oct. 1985.
[20] O. Coudert, C. Berthet, and J.C. Madre, "Verification of sequential machines using Boolean functional vectors," inProc. IMEC-IFIP Int. Workshop Appl. Formal Methods for Correct VLSI Design, Nov. 1989, pp. 111-128.
[21] S. Fortune, J. Hopcroft, and E. M. Schmidt, "The complexity of equivalence and containment for free variable program schemes," inLecture Notes in Computer Science, no. 62, Goos, Hartmanis, Ausiello, and Bohm, Eds. Berlin, Germany: Springer-Verlag, pp. 227-240.
[22] M. Fujita, H. Fujisawa, and N. Kawato, "Evaluations and improvements of a Boolean comparison program based on binary decision diagrams," inProc. Int. Conf. Comput.-Aided Design, 1988, pp. 2-5.
[23] M. Fujita, Y. Matsunaga, and T. Kakuda, "Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagram," inProc. IEEE Int. Conf. Comput.-Aided Design, 1990, pp. 38-41.
[24] H. Fujiwara and S. Toida, "The complexity of fault detection problems for combinational logic circuits,"IEEE Trans. Comput., vol. C-31, pp. 555-560, 1982.
[25] M. R. Garey and D. S. Johnson,Computers and Intractability: A Guide to the Theory of NP-Completeness. San Francisco, CA: Freeman.
[26] H. B. Hunt III and R. E. Stearns, "Monotone Boolean formulae, distributive lattices, and the complexity of logics, algebraic structures, and computation structures," inProc. STACS86, 3rd Annu. Symp. Theoret. Aspects Comput. Sci., vol. 210, B. Monien and G. Vidal-Naquet, Eds. Berlin, Germany, Springer-Verlag, 1986, pp. 282-291.
[27] O. P. Kuznetsov, "Program realization of logical functions and automata Part 1: Analysis and synthesis of binary processes,"Automata and Remote Contr., vol. 38, pp. 1077-1087, 1977.
[28] C. Lee, "Representation of switching circuits by binary decision programs,"Bell Syst. Tech. J., vol. 38, pp. 985-999, July 1959.
[29] S. Malik, A. Wang, R. K. Brayton, and A. Sangiovanni-Vincentelli, "Logic verification using binary decision diagrams in a logic synthesis environment," inProc. Int. Conf. Comput.-Aided Design, 1988, pp. 6-9.
[30] Y. Matsunaga and M. Fujita, "Multilevel logic optimization using binary decision diagrams, " inProc. IEEE Int. Conf. Comput.-Aided Design, 1989, pp. 556-559.
[31] H. Sato, Y. Yasue, Y. Matsunaga, and M. Fujita, "Boolean resubstitution with permissible functions and binary decision diagrams," inProc. 27th IEEE/ACM Design Automation Conf., 1990, pp. 284-289.
[32] H. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, "Implicit state enumeration of finite state machines using BDD's," inProc. IEEE Int. Conf. Comput.-Aided Design, Nov. 1990, pp. 130-133.
[33] J. Wegner, "Time-space tradeoffs for branching programs,"J. Comput. Syst. Sci., vol. 32, no. 1, pp. 91-96, Feb. 1986.

Index Terms:
characterization; binary decision diagrams; Boolean functions; synthesis; simulation; testing; complexity; computational problems; repeated variables; Boolean functions; logic circuits; logic design; logic testing.
Citation:
S. Chakravarty, "A Characterization of Binary Decision Diagrams," IEEE Transactions on Computers, vol. 42, no. 2, pp. 129-137, Feb. 1993, doi:10.1109/12.204789
Usage of this product signifies your acceptance of the Terms of Use.