Abstract
We present a class of Ordered Binary Decision Diagrams, Differential BDDs (δBDDs), and transformations Push-up (↑) and Delta (δ) over them. In addition to the ordinary node-sharing in normal BDDs, isomorphic substructures can be collapsed further in δBDDs and their derived classes, forming a more compact representation of boolean functions. The elimination of isomorphic substructures coincides with the repetitive occurrences of small components in many applications of BDDs. The reduction is potentially exponential in the number of nodes and proportional to the number of variables, while operations on δBDDs remain efficient.
This research was supported in part by the National Science Foundation under grant CCR-92-23226, the Advanced Research Projects Agency under NASA grant NAG2-892, the United States Air Force Office of Scientific Research under grant F49620-93-1-0139, and the Department of the Army under grant DAAH04-95-1-0317.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Akers, S.. Binary decision diagrams. IEEE Transactions on Computers 6, 27 (June 1978), 509–516.
Ashar, P., Ghosh, A., and Devadas, S. Boolean satisfiability and equivalence checking using general binary decision diagrams. In IEEE International Conf. on Computer Design: VLSI in Computers and Processors (1991), pp. 259–264.
Bani-Eqbal, B. Exclusive normal form of boolean circuits. Tech. Rep. UMCS-92-4-1, Department of Computer Science, University of Manchester, 1992.
Becker, B., Bryant, R., Coudert, O., and Meinel, C., Eds. Report on the Third Workshop on Computer Aided Design and Test (Feb. 1995). http: //www. informatik. uni-trier. de/Design_and_Test/.
Becker, B., Drechsler, R., and Theobald, M. OKFDDs versus OBDDs and OFDDs. In International Colloquium on Automata, Languages and Programming (July 1995), LNCS. To appear.
Bern, J., Meinel, C., and Slobodová, A. Efficient OBDD-based boolean manipulation in CAD beyond current limits. In 32ndDesign Automation Conf. (1995).
Bitner, J., Jain, J., Abadir, M., Abraham, J., and Fussell, D. Efficient algorithmic computation using indexed BDDs. In 24thIntl. Symposium on Fault-Tolerant Computing (1994), pp. 266–275.
Brace, K. S., Rudell, R. L., and Bryant, R. E. Efficient implementation of a BDD package. In 27thDesign Automation Conf. (1990), pp. 40–45.
Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers 35, 8 (Aug. 1986), 677–691.
Bryant, R. E. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. on Computers 40, 2 (Feb. 1991), 205–213.
Bryant, R. E. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24, 3 (Sept. 1992), 293–318.
Bryant, R. E., And Chen, Y.-A. Verification of arithmetic circuits with Binary Moment Diagrams. In 32nd Design Automation Conf. (June 1995). To appear.
Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. Symbolic modelchecking: 1020 states and beyond. Information and Computation 98, 2 (June 1992), 142–170.
Clarke, E. M., McMillan, K., Zhao, X., Fujita, M., and Yang, J. Spectral transforms for large Boolean functions with applications to technology mapping. In 30thDesign Automation Conf. (June 1993).
Jeong, S., Plessier, B., Hachtel, G., and Somenzi, F. Extended BDD's: Trading off canonicity for structure in verification algorithms. In IEEE Intl. Conf. on Computer-Aided Design (1991), pp. 464–467.
Kam, T. Y. K., and Brayton, R. K. Multi-valued decision diagrams. Technical Report UCB/ERL M90/125, University of California, Berkeley, Dec. 1990.
Karplus, K. Using if-then-else DAGs for multi-level logic minimization. In Advance Research in VLSI (1989), C. Seitz, Ed., MIT Press, pp. 101–118.
Lai, Y.-T., AND Sastry, S. Edge-valued binary decision diagrams for multi-level hierarchical verification. In 29thDesign Automation Conf. (1992), pp. 608–613.
Madre, J., and Billon, J. Proving circuit correctness using formal comparison between expected and extracted behaviour. In 25thDesign Automation Conf. (June 1988), pp. 205–210.
McMillan, K. L. Hierarchical representations of discrete functions, with application to model checking. In Proc. 6th Intl. Conf. on Computer-Aided Verification (June 1994), vol. 818 of LNCS, Springer-Verlag, pp. 41–54.
Minato, S. Zero-supressed BDDs for set manipulation in combinatorial problems. In 30thDesign Automation Conf. (1993), pp. 272–277.
Minato, S., Ishiura, N., and Jajima, S. Shared binary decision diagram with attributed edges for efficient boolean function manipulation. In 27thDesign Automation Conf. (1990), pp. 52–57.
Possega, J., AND Ludäscher, B. Towards first-order deduction based on Shannon graphs. In Proc. 16thGerman Conf. on AI (GWAI-92) (1992), vol. 671 of LNAI, Springer-Verlag, pp. 67–76.
Sieling, D., AND Wegener, I. Graph driven BDDs—a new data structure for boolean functions. Theoretical Comput. Sci. 141, 2 (Apr. 1995).
Uribe, T. E., and Stickel, M. E. Ordered binary decision diagrams and the Davis-Putnam procedure. In Proc. 1stIntl. Conf. on Constraints in Computational Logics(Sept. 1994), vol. 845 of LNCS, pp. 34–49
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Anuchitanukul, A., Manna, Z., Uribe, T.E. (1995). Differential BDDs. In: van Leeuwen, J. (eds) Computer Science Today. Lecture Notes in Computer Science, vol 1000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015246
Download citation
DOI: https://doi.org/10.1007/BFb0015246
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60105-0
Online ISBN: 978-3-540-49435-5
eBook Packages: Springer Book Archive