Skip to main content
SpringerLink
Log in

OKFDDs — Algorithms, Applications and Extensions

  • Chapter
Representations of Discrete Functions

Abstract

We present Ordered Kronecker Functional Decision Diagrams (OKFDDs), a graph-based data structure for the representation and manipulation of Boolean functions. OKFDDs are a generalization of Ordered Binary Decision Diagrams and Ordered Functional Decision Diagrams and as such provide a more compact representation of the functions than either of the two decision diagrams. We review basic properties of OKFDDs and study methods for their efficient representation and manipulation. These algorithms are integrated in our OKFDD package PUMA whose implementation is briefly discussed. Finally we point out some applications of OKFDDs, demonstrate the efficiency of our approach by some experiments and discuss a promising extension of the concept to also allow representation and manipulation of word-level functions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. B. Becker and R. Drechsler, “How many decomposition types do we need?,” Proc. European Design & Test Conf., pp. 438–443, Mar. 1995.

    Google Scholar 

  2. B. Becker and R. Drechsler, “Synthesis for testability: Circuits derived from ordered kronecker functional decision diagrams,” Proc. European Design & Test Conf., page 592, Mar. 1995.

    Google Scholar 

  3. B. Becker, R. Drechsler, and M. Theobald, “On the implementation of a package for efficient representation and manipulation of functional decision diagrams,” IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pp. 162–169, Sept. 1993.

    Google Scholar 

  4. B. Becker, R. Drechsler, and M. Theobald, “OKFDDs versus OBDDs and OFDDs,” ICALP, LNCS 944, pp. 475–486, July 1995.

    MathSciNet  Google Scholar 

  5. B. Becker, R. Drechsler, and R. Werchner, “On the relation between BDDs and FDDs,” LATIN, LNCS 911, pp. 72–83, Apr. 1995.

    Google Scholar 

  6. B. Bollig, P. Savicky, and I. Wegener, “On the improvement of variable orderings for OBDDs,” IFIP Workshop on Logic and Architecture Synthesis, pp. 71–80, Dec. 1994.

    Google Scholar 

  7. K.S. Brace, R.L. Rudell, and R.E. Bryant, “Efficient implementation of a BDD package,” Proc. Design Automation Conf., pp. 40–45, June 1990.

    Google Scholar 

  8. R.E. Bryant, “Graph — based algorithms for Boolean function manipulation,” IEEE Trans. Comput., vol. C-35, pp. 677–691, Aug. 1986.

    Article  Google Scholar 

  9. R.E. Bryant, “Symbolic boolean manipulation with ordered binary decision diagrams,” ACM, Comp. Surveys, 24:293–318, 1992.

    Article  Google Scholar 

  10. R.E. Bryant and Y.-A. Chen, “Verification of arithmetic functions with binary moment diagrams,” Proc. Design Automation Conf.., pp. 535–541, June 1995.

    Google Scholar 

  11. E.M. Clarke, M. Fujita, and X. Zaho, “Application of multi-terminal binary decision diagrams,” IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pp. 21–27, Aug. 1995. (Also Chapter 4 of this book).

    Google Scholar 

  12. E.M. Clarke, K. McMillan, X. Zhao, M. Fujita, and J. Yang, “Spectral transforms for large boolean functions with application to technology mapping,” Proc. Design Automation Conf., pp. 54–60, June 1993.

    Google Scholar 

  13. E.M. Clarke and X. Zaho, “Word level symbolic model checking — a new approach for verifying arithmetic circuits,” Technical report, CMU-CS-95-161, May 1995.

    Google Scholar 

  14. M. Davio, J.P. Deschamps, and A. Thayse, Discrete and Switching Functions. McGraw-Hill, 1978.

    MATH  Google Scholar 

  15. R. Drechsler and B.Becker, “Dynamic minimization of OKFDDs,” Proc. Int’l Conf. on Comp. Design, pp. 602–607, Oct. 1995.

    Google Scholar 

  16. R. Drechsler and B. Becker, “Rapid prototyping of fully testable multilevel AND/EXOR networks,” IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pp. 126–133, Sept. 1993.

    Google Scholar 

  17. R. Drechsler and B. Becker, “Sympathy: Fast exact minimization of Fixed Polarity Reed-Muller expressions for symmetric functions,” Proc. European Design & Test Conf., pp. 91–97, Mar. 1995.

    Google Scholar 

  18. R. Drechsler, B. Becker, and N. Gockel, “A genetic algorithm for minimization of Fixed Polarity Reed-Muller expressions,” Proc. Int’l Conf. on Artificial Neural Networks and Genetic Algorithms, pp. 392–395, Feb. 1995.

    Google Scholar 

  19. R. Drechsler, B. Becker, and N. Göckel, “A genetic algorithm for 2-Level AND/EXOR minimization,” Proc. SASIMI, pp. 49–56, Aug. 1995.

    Google Scholar 

  20. R. Drechsler, B. Becker, and N. Göckel, “A genetic algorithm for RKRO minimization,” Proc. InVl Symp. on Artificial Intelligence, pp. 266–275, Oct. 1995.

    Google Scholar 

  21. R. Drechsler, B. Becker, and A. Jahnke, “On variable ordering and decomposition type choice in OKFDDs,” Proc. IFIP International Conference on VLSI’95, pp. 805–810, Aug. 1995.

    Google Scholar 

  22. R. Drechsler, B. Becker, and S. Ruppertz, “K✶BMDs: a new data structure for verification,” Proc. European Design & Test Conf., Mar. 1996.

    Google Scholar 

  23. R. Drechsler, B. Becker, and S. Ruppertz, “Dynamic Minimization of K✶BMDs,” submitted, 1995.

    Google Scholar 

  24. R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M.A. Perkowski, “Efficient representation and manipulation of switching functions based on Ordered Kro-necker Functional Decision Diagrams,” Proc. Design Automation Conf., pp. 415–419, June 1994.

    Google Scholar 

  25. R. Drechsler, M. Theobald, and B. Becker, “Fast OFDD based minimization of Fixed Polarity Reed-Muller expressions,” to be published in IEEE Trans. Cornput., 1996.

    Google Scholar 

  26. R. Enders, “Note on the complexity of binary moment diagram representations,” IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pp. 191–197, Aug. 1995.

    Google Scholar 

  27. S.J. Friedman and K.J. Supowit, “Finding the optimal variable ordering for binary decision diagrams,” Proc. Design Automation Conf., pp. 348–356, June 1987.

    Google Scholar 

  28. H. Fujii, G. Ootomo, and C. Hori, “Interleaving based variable ordering methods for ordered binary decision diagrams,” Proc. InVl Conf. on CAD, pp. 38–41, Nov. 1993.

    Google Scholar 

  29. M. Fujita, Y. Matsunga, and T. Kakuda, “On variable ordering of binary decision diagrams for the application of multilevel synthesis,” Proc. European Conf. on Design Automation, pp. 50–54, Mar. 1991.

    Google Scholar 

  30. P. Ho and M.A. Perkowski, “Free kronecker decision diagrams and their application to Atmel 6000 FPGA mapping,” Proc. European Design Automation Conf., pp. 8–13, Sept. 1994.

    Google Scholar 

  31. U. Kebschull, E. Schubert, and W. Rosenstiel, “Multilevel logic synthesis based on functional decision diagrams,” Proc. European Conf. on Design Automation, pp. 43–47, Mar. 1992.

    Google Scholar 

  32. D.P. Appenzeller and A. Kuehlmann, “Formal verification of a PowerPc microprocessor,” Proc. Intl Conf. on Comp. Design, pp. 79–84, Oct. 1995.

    Google Scholar 

  33. V.V. Le, T. Besson, A. Abbara, D. Brasen, H. Bogushevitsh, G. Saucier, and M. Crastes, “ASIC prototyping with area oriented mapping for ALTERA/FLEX devices,” Proc. SASIMI, pp. 176–183, Aug. 1995.

    Google Scholar 

  34. Y.-T. Lai and S. Sastry, “Edge-valued binary decision diagrams for multi-level hierarchical verification,” Proc. Design Automation Conf., pp. 608–613, June 1992. (Also Chapter 5 of this book).

    Google Scholar 

  35. S. Malik, A.R. Wang, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, “Logic verification using binary decision diagrams in a logic synthesis environment,” Proc. Int’l Conf. on CAD, pp. 6–9, Nov. 1988.

    Google Scholar 

  36. S. Minato, “Zero-suppressed BDDs for set manipulation in combinational problems,” Proc. Design Automation Conf., pp. 272–277, June 1993. (Also Chapter 1 of this book).

    Google Scholar 

  37. S. Minato, N. Ishiura, and S. Yajima, “Shared binary decision diagrams with attributed edges for efficient boolean function manipulation,” Proc. Design Automation Conf., pp. 52–57, June 1990.

    Google Scholar 

  38. Richard Rudell, “Dynamic variable ordering for ordered binary decision diagrams,” Proc. Int’l Conf. on CAD, pp. 42–47, Nov. 1993.

    Google Scholar 

  39. T. Sasao, Logic Synthesis and Optimization. Kluwer Academic Publisher, 1993. (Also Chapter 2 of this book).

    Book  Google Scholar 

  40. I. Schaefer, M.A. Perkowski, and H.Wu, “Multilevel logic synthesis for cellular FPGAs based on orthogonal expansions,” IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pp. 42–51, Sept. 1993.

    Google Scholar 

  41. H. Touati, H. Savoj, B. Lin, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, “Implicit enumeration of finite state machines using BDDs,” Proc. Int’l Conf. on CAD, pp. 130–133, Nov. 1990.

    Google Scholar 

  42. R. Werchner, T. Harich, R. Drechsler, and B. Becker, “Satisfiability problems for ordered functional decision diagrams,” IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in Circuit Design, pp. 206–212, Aug. 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Albert-Ludwigs-University, 79110, Freiburg im Breisgau, Germany

    Rolf Drechsler & Bernd Becker

Authors
  1. Rolf Drechsler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd Becker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Electronics, Kyushu Institute of Technology, Iizuka, Japan

    Tsutomu Sasao

  2. Fujitsu Laboratories of America Inc., Santa Clara, California, USA

    Masahiro Fujita

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Kluwer Academic Publishers

About this chapter

Cite this chapter

Drechsler, R., Becker, B. (1996). OKFDDs — Algorithms, Applications and Extensions. In: Sasao, T., Fujita, M. (eds) Representations of Discrete Functions. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-1385-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-1-4613-1385-4_7

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4612-8599-1

  • Online ISBN: 978-1-4613-1385-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation