This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Efficient Boolean Manipulation with OBDD's Can be Extended to FBDD's
October 1994 (vol. 43 no. 10)
pp. 1197-1209

OBDD's are the state-of-the-art data structure for Boolean function manipulation. Basic tasks of Boolean manipulation such as equivalence test, satisfiability test, tautology test and single Boolean synthesis steps can be performed efficiently in terms of fixed ordered OBDD's. The bottleneck of most OBDD-applications is the size of the represented Boolean functions since the total computation merely remains tractable as long as the OBDD-representations remain of reasonable size. Since it is well known that OBDD's are restricted FBDD's (free BDD's, i.e., BDD's that test, on each path, each input variable at most once), and that FBDD-representations are often much more (sometimes even exponentially more) concise than OBDD-representations. We propose to work with a more general FBDD-based data structure. We show that FBDD's of a fixed type provide, similar as OBDD's of a fixed variable ordering, canonical representations of Boolean functions, and that basic tasks of Boolean manipulation can be performed in terms of fixed typed FBDD's similarly efficient as in terms of fixed ordered OBDD's. In order to demonstrate the power of the FBDD-concept we show that the verification of the circuit design for the hidden weighted bit function proposed Bryant can be carried out efficiently in terms of FBDD's while this is, for principal reasons, impossible in terms of OBDD's.

[1] P. Ashar, S. Devadas, and A. Ghosh, "Boolean satisfiability and equivalence checking using general binary decision diagrams," inProc. Int. Conf. Comput. Design, Cambridge, MA, Oct. 1991, 259-264.
[2] P. Ashar, S. Devadas, and K. Keutzer, "Gate-delay-fault testability properties of multiplexor-based networks, " inProc. Int. Test Conf., 1991, pp. 887-896.
[3] S. B. Akers, "Binary decision diagrams,"IEEE Trans. Comput., vol. C-27, no. 6, pp. 509-516, Aug. 1978.
[4] J. B. Burchet al., "Symbolic model checking: 1020states and beyond," inProc. 5th Symp. Logics in Computer Science, pp. 428-439, IEEE Computer Society Press, 1990.
[5] J.R. Burch et al., "Sequential Circuit Verification Using Symbolic Model Checking,"Proc. 27th Design Automation Conf., IEEE CS Press, 1990, pp. 46-51.
[6] 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.
[7] B. Becker, "Synthesis for testability, binary decision diagrams," inProc. 9th Annu. Symp. Theoretical Aspects of Comput. Sci.(Lecture Notes in Computer Science 577), Feb. 1992, pp. 501-512.
[8] J. Bitner, J. Jain, M. Abadir, J. A. Abraham, and D. S. Fussel, "Efficient verification of multipliers and other different functions using IBDD's,"Proc. Custom Integrated Circuits Conf., May 1992.
[9] Y. Breitbart, H. B. Hunt, III, and D. Rosenkrantz, "The size of binary decision diagrams representing Boolean functions," manuscript, 1991.
[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] K. M. Butler, D. E. Ross, R. Kapur, and M. R. Mercer, "Heuristics to compute variable orderings for efficient manipulation of ordered binary decision diagrams," inProc. 28th ACM/IEEE Design Automat. Conf., San Francisco, CA, June 1991, pp. 417-420.
[12] R. E. Bryant, "Graph-based algorithms for Boolean function manipulation,"IEEE Trans. Comput., vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[13] R. E. Bryant, "On the complexity of VLSI implementations and graph representations of Boolean functions with applications to integer multiplication,"IEEE Trans. Comput., vol. 40, no. 2, pp. 205-213, Feb. 1991.
[14] R. E. Bryant, "Symbolic boolean manipulation with ordered binary-decision diagrams,"ACM Computing Surveysvol. 24, no. 3, pp. 293-318, 1992.
[15] R. E. Bryant, personal communication, June 1992.
[16] R. L. Constable, H. B. Hunt, III, and S. Sahni, "On the computational complexity of scheme equivalence," inProc. 8th Princeton Conf. Inform. Sci. and Syst., 1974.
[17] O. Coudert, J. C. Madre, and C. Berthet, "Verifying temporal properties of sequential machines without building their state diagrams." inInt. Workshop on Computer-Aided Verification, June 1990.
[18] H. Eveking,Verifikation digitaler Systeme, Stuttgart: Teubner, 1991.
[19] 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.
[20] 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.
[21] 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.
[22] S. J. Friedman and K. J. Supowit, "Finding the optimal variable ordering for binary decision diagrams,"IEEE Trans. Comput.vol. 39, pp. 710-713, 1990.
[23] M. R. Garey and D. Johnson,Computers and Intractability. New York: W. H. Freeman, 1978.
[24] J. Gergov and Ch. Meinel, "Analysis and manipulation of Boolean functions in terms of decision graphs," inProc. 18th Inc. Workshop on Graph-Theoretic Concepts in Comput. Sci.(Lecture Notes in Computer Science) vol. 657, pp. 310-320, 1993. Also inIPL, vol. 50, pp. 317-322, 1994.
[25] J. Gergov and Ch. Meinel, "Efficient analysis and manipulation of OBDD's can be extended to read-once-only branching programs," Tech. Rep. 92-10, Univ. of Trier, June 1992.
[26] J. Gergov and C. Meinel, "Frontiers of feasible boolean manipulation with branching programs," in10th Symp. Theoretical Aspects of Comput. Sci., (Lecture Notes in Computer Science 665), 1993, pp. 576-585.
[27] J. Gergov and Ch. Meinel, "Computational logic verification with FBDD' s," Tech. Rep. 93-08, Univ. of Trier, Apr. 1993.
[28] J. Jain, J. bitner, j. abraham, and d. s. fussell, "functional partitioning for verification and related problems," inProc. Brown/MIT VLSI Conf., Mar, 1992, pp. 210-226.
[29] S.-W. Jeong, B. Plessier, G. Hachtel, and F. Somenzi, "Extended BDD's, trading off canonicity for structure in verification algorithms," inProc. Int. Conf. Comput.-Aided Design, Santa Clara, CA, Nov. 1991, pp. 464-467.
[30] K. Karplus, "Using if-then-else DAGs for multi-level logic minimization," inProc. Advanced Research in VLSI, C. Seitz Ed. Cambridge, MA: MIT Press, 1989, pp. 101-118.
[31] R. Krieger, "PLATO, a tool for computation of exact signal probabilities," inProc. VLSI Design Conf., 1993., pp. 65-68
[32] R. Krieger, B. Becker, and R. Sinkovic´, "A BDD-based algorithm for computation of exact fault detection probabilities," inProc. Int. Symp. Fault-Tolerant Computing, 1993.
[33] Ch. Meinel,Modified Branching Programs and Their Computational Power(Lecture Notes in Computer Science). Berlin: Springer-Verlag, 1989, vol. 370.
[34] Ch. Meinel, "Branching programs-An efficient data structure for computer-aided circuit design,"EATCS Bull., no. 46, pp. 149-170, 1992.
[35] S. Minato, I. Ishiura, and S. Yajima, "Shared binary decision diagrams with attributed edges for efficient Boolean function manipulation," inProc. 27th ACM/IEEE Design Automat. Conf., Orlando, FL, June 1990, pp. 52-57.
[36] 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.
[37] D. Sieling and I. Wegener, "Graph driven BDD's-A new data structure for Boolean functions," manuscript, Aug. 1992.

Index Terms:
Boolean functions; logic design; data structures; Boolean manipulation; OBDD; data structure; Boolean function manipulation; equivalence test; satisfiability test; tautology test; total computation; canonical representations; circuit design.
Citation:
J. Gergov, C. Meinel, "Efficient Boolean Manipulation with OBDD's Can be Extended to FBDD's," IEEE Transactions on Computers, vol. 43, no. 10, pp. 1197-1209, Oct. 1994, doi:10.1109/12.324545
Usage of this product signifies your acceptance of the Terms of Use.