
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
S.i. Minato, "Streaming BDD Manipulation," IEEE Transactions on Computers, vol. 51, no. 5, pp. 474485, May, 2002.  
BibTex  x  
@article{ 10.1109/TC.2002.1004587, author = {S.i. Minato}, title = {Streaming BDD Manipulation}, journal ={IEEE Transactions on Computers}, volume = {51}, number = {5}, issn = {00189340}, year = {2002}, pages = {474485}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2002.1004587}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Streaming BDD Manipulation IS  5 SN  00189340 SP474 EP485 EPD  474485 A1  S.i. Minato, PY  2002 KW  BDD KW  binary decision diagram KW  VLSI CAD KW  logic design KW  verification KW  testing KW  data structure KW  algorithm KW  combinatorial problem VL  51 JA  IEEE Transactions on Computers ER   
Binary Decision Diagrams (BDDs) are now commonly used for handling Boolean functions because of their excellent efficiency in terms of time and space. However, the conventional BDD manipulation algorithm is strongly based on the hash table technique, so it always encounters the memory overflow problem when handling largescale BDD data. This paper proposes a new streaming BDD manipulation method that never causes memory overflow or swap out. This method allows us to handle very largescale BDD stream data beyond the memory limitation. Our method can be characterized as follows: 1) it gives a continuous tradeoff curve between memory usage and stream data length, 2) valid solutions for a partial Boolean space can be obtained if we break the process before finishing, and 3) easily accelerated by pipelined multiprocessing. An experimental result demonstrates that we can succeed in finding a number of solutions to a SAT problem using commodity PC with a 64 MB memory, where as the conventional BDD manipulator would have required a 100GB memory. BDD manipulation has been considered as an intensively memoryconsuming procedure, but now we can also utilize the hard disk and network resources as well. The method leads to a new approach to BDD manipulation.
[1] T. Bell, I.H. Witten, and J.G. Cleary, “Modeling for Text Compression,” ACM Computing Surveys, vol. 21, no. 4, pp. 557591, Dec. 1989.
[2] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs Proc. Tools and Algorithms for the Construction and Analysis of Systems, 1999.
[3] K.S. Brace, R.L. Rudell, and R.E. Bryant, Efficient Implementation of a BDD Package Proc. Design Automation Conf., pp. 4045, 1990.
[4] R.E. Bryant, "GraphBased Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C35, No. 8, Aug. 1986, pp. 667690.
[5] J. Burch, E. Clarke, K. McMillan, and D. Dill, "Sequential Circuit Verification Using Symbolic Model Checking," Proc. 27th Design Automation Conf., pp. 4651, 1990.
[6] E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang, "Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping," Proc. 30th Design Automation Conf., pp. 5460, 1993.
[7] G. Janssen, “Design of a Pointerless BDD Package,” Note of Int'l Workshop Logic and Synthesis (IWLS2001), May 2001.
[8] S. Kimura and E.M. Clarke, “A Parallel Algorithm for Constructing Binary Decision Diagrams,” Proc. IEEE/ACM Int'l Conf. Computer Design (ICCD90), pp. 220223, Sept. 1990.
[9] YT. Lai, M. Pedram, and S. Sastry (S.B.K. Vrudhula), "FGILP: An integer linear program solver based on function graphs," Proc. Int'l Conf. Computer Aided Design, 1993.
[10] M. Löbbing, and I. Wegener, “The Number of Knight's Tour Equals$33,439,123,484,294$—Counting with Binary Decision Diagrams,” The Electric J. Combinatorics, vol. 3, no. R5, 1996.
[11] D.E. Long, “The Design of a CacheFriendly BDD Library,” Proc. IEEE/ACM Int'l Conf. ComputerAided Design (ICCAD98), pp. 639645, Nov. 1998.
[12] J.C. Madre and O. Coudert, “A Logically Complete Reasoning Maintenance System Based on a Logical Constraint Solver,” Proc. Int'l Joint Conf. Artificial Intelligence (IJCAI), pp. 294299, 1991.
[13] K. MilvangJensen and A.J. Hu, “BDDNOW: A Parallel BDD Package,” Formal Method in ComputerAided Design (Proc. FMCAD98), pp. 501507, June 1998.
[14] S. Minato, “BEMII: An Arithmetic Boolean Expression Manipulator Using BDDs,” IEICE Trans. Fundamentals, vol. E76A, no. 10, pp. 17211729, Oct. 1993.
[15] S. Minato, N. Ishiura, and S. Yajima, Shared Binary Decision Diagrams with Attributed Edges for Efficient Boolean Function Manipulation Proc. Design Automation Conf., pp. 5257, 1990.
[16] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and A. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. 38th ACM/IEEE Design Automation Conf. (DAC2001), pp. 530535, June 2001.
[17] H. Ochi, Y. Kouichi, and S. Yajima, “BreadthFirst Manipulation of Very Large BinaryDecision Diagrams,” Proc. IEEE/ACM Int'l Conf. ComputerAided Design (ICCAD93), pp. 4855, Nov. 1993.
[18] H.G. Okuno, “Reducing Combinatorial Explosions in Solving SearchType Combinatorial Problems with Binary Decision Diagram,” Trans. of Information Processing Soc. Japan (IPSJ), (in Japanese), vol. 35, no. 5, pp. 739753, May 1994.
[19] R.K. Ranjan, J.V. Sanghavi, R.K. Brayton, and A. SangiovanniVincentelli, “Binary Decision Diagrams on Network of Workstations,” Proc. IEEE/ACM Int'l Conf. Computer Design (ICCD96), Oct. 1996.
[20] B. Selman, H. Levesque, and D. Mitchell, “A New Method for Solving Hard Satisfiability Problems,” Proc. Am. Assoc. Artificial Intelligence, (AAAI '92), pp. 440446, July 1992.
[21] J.P. MarquesSilva and K.A. Sakallah, "Grasp: A New Search Algorithm for Satisfiability," Proc. Int'l Conf. ComputerAided Design (ICCAD 96), IEEE CS Press, 1996, pp. 220227.
[22] F. Somenzi, “Efficient Manipulation of Decision Diagrams,” Int'l J. Software Tools for Technology Transfer (STTT), vol. 3, no.2, pp. 171181, May 2001.
[23] F. Somenzi et al. “CUDD: CU Decision Diagram Package,” Public Software,http://vlsi.colorad.edu/fabioCUDD,YEAR???
[24] T. Stornetta and F. Brewer, “Implementation of an Efficient Paralell BDD Package,” Proc. 33th ACM/IEEE Design Automation Conf. (DAC '96), June 1996.
[25] M.N. Velev and R.E. Bryant, “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessor,” Proc. 38th ACM/IEEE Design Automation Conf. (DAC2001), pp. 226231, June 2001.
[26] B. Yang, Y.A. Chen, R.E. Bryant, and D.R. O'Hallaron, “Space and Timeefficient BDD Construction via Working Set Control,” Proc. Asia and South Pacific Design Autonation Conf. (ASPDAC98), pp. 423432, Feb. 1998.
[27] J. Ziv and A. Lempel, "A Universal Algorithm for Sequential Data Compression," IEEE Trans. Information Theory, vol. 23, no. 3, pp. 337343, 1977.