Abstract
Graph-based symbolic techniques are part of many synthesis and verification tools. Problems occur if an application requires multiple graph types to model complex designs, since there are many exponential gaps (for time and space) between different types of decision diagrams.
This paper presents hybrid graph manipulation algorithms that integrate common decision diagrams into a single graph manipulation package. An important feature of the presented work is that graph operations are no longer restricted to a single graph type or to a single decomposition type list. Operations on multiple graph types are using an implicit type conversion scheme that prevents from many exponential gaps between different types of decision diagrams.
The package implementation provides the graph types BDD, FDD, OKFDD, MTBDD, EVBDD, BMD, *BMD, p*BMD, HDD, K*BMD and ZDD in order to represent boolean and integer functions as well as sets. Applications of the presented method exist virtually in any approach based on decision diagrams. The paper investigates manipulation of bit-level and word-level functions as well as bit selection from arithmetic expressions.
A convenient extension of DD packages is the ability to dynamically adapt variable ordering. This technique called ‘sifting’ has been first introduced for BDDs. This paper defines an extension to *BMDs, called positive *BMDs (p*BMDs), that allows for dynamic variable reordering. Reordering techniques in the package can be applied even if multiple graph types are used together.
Chapter PDF
Similar content being viewed by others
References
L. Arditi. *BMDs can delay the use of theorem proving for verifying arithmetic assembly instructions. Formal Methods in Computer-Aided Design, pages 34–48, November 1996.
B. Becker and R. Drechsler. How many decomposition types do we need? European Design and Test Conference, pages 438–443, 1995.
B. Becker, R. Drechsler, and R. Enders. On the representational power of bit-level and word-level decision diagrams. Asian and South Pacific Design Automation Conference, 1997.
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C(35): 677–691, August 1986.
R. E. Bryant and Y.-A. Chen. Verification of arithmethic functions with binary moment diagrams. Technical Report CMU-CS-94–160, Carnegie Mellon University, May 1994.
R. E. Bryant and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. ACM/IEEE Design Automation Conference, pages 535–541, 1995.
E. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams — overcoming the limitations of MTBDDs and BMDs. International Conference on Computer Aided Design, November 1995.
E. Clarke, K. L. McMillan, X. Zhao, and J. C.-Y. Yang. Spectral transforms for large Boolean functions with application to technology mapping. ACM/IEEE Design Automation Conference, pages 54–60, June 1993.
E. Clarke, M. Kaira, and X. Zhao. Word level model checking — avoiding the pentium fdiv error. ACM/IEEE Design Automation Conference, pages 645–648, June 1996.
R. Drechsler and B. Becker. Dynamic minimization of OKFDDs. In International Conference on Computer Design, pages 602–607, 1995.
R. Drechsler, B. Becker, and S. Ruppertz. K*BMDs a new data structure for verification. European Design and Test Conference, 1996.
R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M. A. Perkowski. Efficient representation and manipulation of switching functions based on ordered kronecker functional decision diagrams. ACM/IEEE Design Automation Conference, pages 415–419, 1994.
N. Ishiura, H. Sawada, and S. Yajima. Minimization of binary decision diagrams based on exchanges of variables. International Conference on Computer-Aided Design, pages 472–475, 1991.
U. Kebschull, E. Schubert, and W. Rosenstiel. Multilevel logic synthesis based on functional decision diagrams. European Conference on Design Automation, pages 43–47, 1992.
Y.T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. ACM/IEEE Design Automation Conference, pages 608–613, June 1992.
S. Minato. Zero-suppressed BDDs for set manipulation in combinational problems. ACM/IEEE Design Automation Conference, pages 272–277, 1993.
R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. International Conference on Computer Aided Design, pages 42–47, 1993.
T. Sasao and M. Fujita (Editors). Representations of Discrete Functions. Kluwer Academic Publishers, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 IFIP
About this chapter
Cite this chapter
Höreth, S. (1997). Implementation of a Multiple-Domain Decision Diagram Package. In: Li, H.F., Probst, D.K. (eds) Advances in Hardware Design and Verification. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35190-2_12
Download citation
DOI: https://doi.org/10.1007/978-0-387-35190-2_12
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2885-8
Online ISBN: 978-0-387-35190-2
eBook Packages: Springer Book Archive