
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 11971209, October, 1994.  
BibTex  x  
@article{ 10.1109/12.324545, author = {J. Gergov and C. Meinel}, title = {Efficient Boolean Manipulation with OBDD's Can be Extended to FBDD's}, journal ={IEEE Transactions on Computers}, volume = {43}, number = {10}, issn = {00189340}, year = {1994}, pages = {11971209}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.324545}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Efficient Boolean Manipulation with OBDD's Can be Extended to FBDD's IS  10 SN  00189340 SP1197 EP1209 EPD  11971209 A1  J. Gergov, A1  C. Meinel, PY  1994 KW  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. VL  43 JA  IEEE Transactions on Computers ER   
OBDD's are the stateoftheart 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 OBDDapplications is the size of the represented Boolean functions since the total computation merely remains tractable as long as the OBDDrepresentations 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 FBDDrepresentations are often much more (sometimes even exponentially more) concise than OBDDrepresentations. We propose to work with a more general FBDDbased 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 FBDDconcept 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, 259264.
[2] P. Ashar, S. Devadas, and K. Keutzer, "Gatedelayfault testability properties of multiplexorbased networks, " inProc. Int. Test Conf., 1991, pp. 887896.
[3] S. B. Akers, "Binary decision diagrams,"IEEE Trans. Comput., vol. C27, no. 6, pp. 509516, Aug. 1978.
[4] J. B. Burchet al., "Symbolic model checking: 1020states and beyond," inProc. 5th Symp. Logics in Computer Science, pp. 428439, 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. 4651.
[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. 8082, 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. 501512.
[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. 4045.
[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. 417420.
[12] R. E. Bryant, "Graphbased algorithms for Boolean function manipulation,"IEEE Trans. Comput., vol. C35, no. 8, pp. 677691, 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. 205213, Feb. 1991.
[14] R. E. Bryant, "Symbolic boolean manipulation with ordered binarydecision diagrams,"ACM Computing Surveysvol. 24, no. 3, pp. 293318, 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 ComputerAided 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: SpringerVerlag, pp. 227240.
[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. 25.
[21] 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.
[22] S. J. Friedman and K. J. Supowit, "Finding the optimal variable ordering for binary decision diagrams,"IEEE Trans. Comput.vol. 39, pp. 710713, 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 GraphTheoretic Concepts in Comput. Sci.(Lecture Notes in Computer Science) vol. 657, pp. 310320, 1993. Also inIPL, vol. 50, pp. 317322, 1994.
[25] J. Gergov and Ch. Meinel, "Efficient analysis and manipulation of OBDD's can be extended to readonceonly branching programs," Tech. Rep. 9210, 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. 576585.
[27] J. Gergov and Ch. Meinel, "Computational logic verification with FBDD' s," Tech. Rep. 9308, 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. 210226.
[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. 464467.
[30] K. Karplus, "Using ifthenelse DAGs for multilevel logic minimization," inProc. Advanced Research in VLSI, C. Seitz Ed. Cambridge, MA: MIT Press, 1989, pp. 101118.
[31] R. Krieger, "PLATO, a tool for computation of exact signal probabilities," inProc. VLSI Design Conf., 1993., pp. 6568
[32] R. Krieger, B. Becker, and R. Sinkovic´, "A BDDbased algorithm for computation of exact fault detection probabilities," inProc. Int. Symp. FaultTolerant Computing, 1993.
[33] Ch. Meinel,Modified Branching Programs and Their Computational Power(Lecture Notes in Computer Science). Berlin: SpringerVerlag, 1989, vol. 370.
[34] Ch. Meinel, "Branching programsAn efficient data structure for computeraided circuit design,"EATCS Bull., no. 46, pp. 149170, 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. 5257.
[36] 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.
[37] D. Sieling and I. Wegener, "Graph driven BDD'sA new data structure for Boolean functions," manuscript, Aug. 1992.