
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
S. Chakravarty, "A Characterization of Binary Decision Diagrams," IEEE Transactions on Computers, vol. 42, no. 2, pp. 129137, February, 1993.  
BibTex  x  
@article{ 10.1109/12.204789, author = {S. Chakravarty}, title = {A Characterization of Binary Decision Diagrams}, journal ={IEEE Transactions on Computers}, volume = {42}, number = {2}, issn = {00189340}, year = {1993}, pages = {129137}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.204789}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  A Characterization of Binary Decision Diagrams IS  2 SN  00189340 SP129 EP137 EPD  129137 A1  S. Chakravarty, PY  1993 KW  characterization; binary decision diagrams; Boolean functions; synthesis; simulation; testing; complexity; computational problems; repeated variables; Boolean functions; logic circuits; logic design; logic testing. VL  42 JA  IEEE Transactions on Computers ER   
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. C35, no. 4, pp. 375379, Apr. 1986.
[2] A. V. Aho and J. D. Ullman,Principles of Compiler Design. Reading, MA: AddisonWesley, 1979.
[3] S. B. Akers, "Binary decision diagrams,"IEEE Trans. Comput., vol. C 27, no. 6, p. 509516, June 1978.
[4] S. B. Akers, "Functional testing using binary decision diagrams," inProc. 8th Int. Symp. Fault Tolerant Comput., June 1978, pp. 8292.
[5] S. B. Akers, "A procedure for functional design verification," inProc. IEEE/ ACM 10th Int. Fault Tolerant Comput. Symp., Oct. 1980, pp. 6567.
[6] P. Ashar, S. Devadas, and K. Keutzer, "Testability properties of multilevel logic networks derived from binary decision diagrams," inProc. Santa Cruz Conf. Advanced Res. VLSI, Mar. 1991, pp. 3554.
[7] C. L. Berman, "Ordered binary decision diagrams and circuit structure," inProc. ICCD, 1989, pp. 392395.
[8] B. Bhattacharya and S.C. Seth, "On the reconvergent structure of combinational circuits with applications to compact testing," inProc. IEEE/ACM 17th Int. FaultTolerant Comput. Symp., 1987, pp. 264269.
[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. 8082, 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. 4045.
[11] R. E. Bryant, "Graphbased algorithms for Boolean function manipulation,"IEEE Trans. Comput., vol. C35, no. 8, pp. 677691, 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. 688694.
[13] R. E. Bryant, "Symbolic verification of MOS circuits," inProc. 1985 Chapel Hill Conf. VLSI, Computer Science Press, pp. 419438.
[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. C40, no. 2, pp. 205213, 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. 4651.
[17] S. Chakravarty and H. B. Hunt III, "On computing signal probability and detection probability for stuckat faults,"IEEE Trans. Comput., vol. 39, no. 11, pp. 13691377, Nov. 1990.
[18] S. Chakravarty, "A testable multiplexer realization of CMOS combinational circuits," inProc. 1989 IEEE Int. Test Conf., pp. 509518.
[19] E. Cerny and J. Gecsei, "Simulation of MOS circuits by decision diagrams,"IEEE Trans. ComputerAided Design, vol. CAD4, pp. 685693, Oct. 1985.
[20] O. Coudert, C. Berthet, and J.C. Madre, "Verification of sequential machines using Boolean functional vectors," inProc. IMECIFIP Int. Workshop Appl. Formal Methods for Correct VLSI Design, Nov. 1989, pp. 111128.
[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: SpringerVerlag, pp. 227240.
[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. 25.
[23] M. Fujita, Y. Matsunaga, and T. Kakuda, "Automatic and semiautomatic verification of switchlevel circuits with temporal logic and binary decision diagram," inProc. IEEE Int. Conf. Comput.Aided Design, 1990, pp. 3841.
[24] H. Fujiwara and S. Toida, "The complexity of fault detection problems for combinational logic circuits,"IEEE Trans. Comput., vol. C31, pp. 555560, 1982.
[25] M. R. Garey and D. S. Johnson,Computers and Intractability: A Guide to the Theory of NPCompleteness. 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. VidalNaquet, Eds. Berlin, Germany, SpringerVerlag, 1986, pp. 282291.
[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. 10771087, 1977.
[28] C. Lee, "Representation of switching circuits by binary decision programs,"Bell Syst. Tech. J., vol. 38, pp. 985999, July 1959.
[29] S. Malik, A. Wang, R. K. Brayton, and A. SangiovanniVincentelli, "Logic verification using binary decision diagrams in a logic synthesis environment," inProc. Int. Conf. Comput.Aided Design, 1988, pp. 69.
[30] Y. Matsunaga and M. Fujita, "Multilevel logic optimization using binary decision diagrams, " inProc. IEEE Int. Conf. Comput.Aided Design, 1989, pp. 556559.
[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. 284289.
[32] H. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. SangiovanniVincentelli, "Implicit state enumeration of finite state machines using BDD's," inProc. IEEE Int. Conf. Comput.Aided Design, Nov. 1990, pp. 130133.
[33] J. Wegner, "Timespace tradeoffs for branching programs,"J. Comput. Syst. Sci., vol. 32, no. 1, pp. 9196, Feb. 1986.