Skip to main content
SpringerLink
Log in

Data Structures for Boolean Functions BDDs — Foundations and Applications

  • Chapter
  • First Online:
Book cover Computational Discrete Mathematics

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2122))

  • 1142 Accesses

Abstract

This article gives an outline of a lecture about ordered binary decision diagrams (OBDDs). Introduced in 1986, OBDDs nowadays are the state-of-the-art data structure for representation of Boolean functions in electronic design automation (EDA).

An overview is given about the data structure, its properties, algorithmic behaviour, and the most important applications. Proofs and technical details have been omitted but can be found all in [28].

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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. J. R. Burch, E. M. Clarke, D. E. Long, Symbolic Model Checking with partitioned transition relations, Proc. of Int. Conf. on VLSI, 1991.

    Google Scholar 

  2. J. Bern, Ch. Meinel, and A. Slobodová. OBDD-based Boolean manipulation in CAD beyond current limits. In Proc. 32nd ACM/IEEE Design Automation Conference (San Francisco, CA), pages 408–413, 1995.

    Google Scholar 

  3. B. Bollig and I. Wegener. Improving the variable ordering of OBDDs is NP-complete. IEEE Transactions on Computers, 45:993–1002, 1996.

    Article  MATH  Google Scholar 

  4. R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35:677–691, 1986.

    Article  Google Scholar 

  5. R. E. Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Transactions on Computers, C-40:205–213, 1991.

    Article  Google Scholar 

  6. R. E. Bryant. Symbolic Boolean manipulation with ordered binary decision diagrams. A CM Computing Surveys, 24(3):293–318, 1992.

    Article  Google Scholar 

  7. O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proc. Workshop on Automatic Verification Methods for Finite State Machines, volume 407 of Lecture Notes in Computer Science, pages 365–373. Springer, 1989.

    Google Scholar 

  8. O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proc. IEEE International Conference on Computer-Aided Design, pages 126–129, 1990.

    Google Scholar 

  9. O. Coudert and J. C. Madre. The implicit set paradigm: A new approach to finite state system verification. Formal Methods in System Design, 6(2):133–145, 1995.

    Article  Google Scholar 

  10. R. Drechsler, W. Günther, Using Lower Bounds During Dynamic BDD Minimization, in Proc of. IEEE International Conference on Computer-Aided Design, pages 29–32, 1999.

    Google Scholar 

  11. E. Dubrova, H. Sack, Probabilistic verification of multiple-valued functions, Proc. of the 30th Int. Symp. on Multiple Valued Logic (ISMVL2000), 2000.

    Google Scholar 

  12. 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. In Proc. 31st ACM/IEEE Design Automation Conference (San Diego, CA), pages 415–419, 1994.

    Google Scholar 

  13. S. J. Friedman and K. J. Supowit. Finding the optimal variable ordering for binary decision diagrams. IEEE Transactions on Computers, 39:710–713, 1990.

    Article  MathSciNet  Google Scholar 

  14. M. R. Garey and M. Johnson. Computers and Intractibility: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1978.

    Google Scholar 

  15. D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In Proc. Computer-Aided Verification, volume 818, pages 299–310, 1994.

    Google Scholar 

  16. J. Gergov and Ch. Meinel. Frontiers of feasible and probabilistic feasible Boolean manipulation with branching programs. In Symposium on Theoretical Aspects in Computer Science, volume 665 of Lecture Notes in Computer Science, pages 576–585. Springer, 1993.

    Google Scholar 

  17. J. Gergov and Ch. Meinel. MOD-2-OBDDs-a data structure that generalizes EXOR-sum-of-products and ordered binary decision diagrams. Formal Methods in System Design, 8:273–282, 1996.

    Article  Google Scholar 

  18. H. Higuchi, F. Somenzi, Lazy Group Sifting for Efficient Symbolic State Traversal of FSMs, in Proc. of IEEE International Conference on Computer-Aided Design, 1999.

    Google Scholar 

  19. J. Jain, W. Adams and M. Fujita, Sampling schemes for computing OBDD variable orderings, Proc. IEEE International Conference on Computer-Aided Design, pages 331–638, 1998.

    Google Scholar 

  20. J. Jain, J. Bitner, D. S. Fussell, J. A. Abraham, Probabilistic verification of Boolean functions, in Formal Methods in System Design 1, Kluwer Academic Publishers, pages 65–116, 1992.

    Google Scholar 

  21. U. Kebschull, E. Schubert, and W. Rosenstiel. Multilevel logic synthesis based on functional decision diagrams. In Proc. European Design Automation Conference, pages 43–47, 1992.

    Google Scholar 

  22. S. Lawrence and C.L. Gilles, Accessibility of information on the web, Nature, Volume 400, Number 6740, 1999.

    Google Scholar 

  23. S. Malik, A. Wang, R. K. Brayton, and A. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Proc. IEEE International Conference on Computer-Aided Design (Santa Clara, CA), pages 6–9, 1988.

    Google Scholar 

  24. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  25. C. Meinel and A. Slobodová, Speeding up Variable Reordering of OBDDs, in Proc. of the International Conference on Computer Design, pages 338–343, 1997.

    Google Scholar 

  26. Ch. Meinel, F. Somenzi, and T. Theobald. Linear sifting of decision diagrams. In Proc. 34th ACM/IEEE Design Automation Conference (Anaheim, CA), pages 202–207, 1997.

    Google Scholar 

  27. Ch. Meinel and T. Theobald. Local encoding transformations for optimizing OBDD-representations of finite state machines. In Proc. International Conference on Formal Methods in Computer-Aided Design (Palo Alto, CA), volume 1166 of Lecture Notes in Computer Science, pages 404–418. Springer, 1996.

    Chapter  Google Scholar 

  28. C. Meinel and T. Theobald, Algorithms and datastructures in VLSI-Design, Springer, 1998.

    Google Scholar 

  29. S. Minato, N. Ishiura, and S. Yajima. Shared binary decision diagrams with attributed edges. In Proc. 27th ACM/IEEE Design Automation Conference (Florida,FL), pages 52–57, 1990.

    Google Scholar 

  30. C. Meinel, H. Sack, b+-OBDDs-a BDD structure for probabilistic verification, in Proc. Workshop on Probabilistic Methods in Verification pages 141–151, 1998.

    Google Scholar 

  31. Ch. Meinel, H. Sack, Algorithmic Considerations for Parity-OBDD Reordering, in Proc. of the 1999 IEEE/ACM Int. Workshop on Logic Synthesis (IWLS99), 1999.

    Google Scholar 

  32. Ch. Meinel, K. Schwettmann, A. Slobodová, Application Driven Variable Reordering and an Example Implementation in Reachability Analysis, in Proc. of ASP-DAC’99, Hongkong, pages 327–330, 1999.

    Google Scholar 

  33. Ch. Meinel, F. Somenzi, T. Theobald Linear Sifting of Decision Diagrams in Proc. of 34th IEEE International Conference on Computer-Aided Design, Anaheim (USA), IEEE Computer Society Press, pages 202–207, 1997.

    Google Scholar 

  34. Ch. Meinel, F. Somenzi, T. Theobald, Function Decomposition and Synthesis Using Linear Sifting, in Proc. ASP-DAC’98, Yokohama (Japan), pages 81–86, 1998.

    Google Scholar 

  35. Ch. Meinel, Ch. Stangier, Speeding up Symbolic Model Checking by Accelerating Dynamic Variable Reordering, in Proc. of 10th ACM Great Lake Symposium on VLSI, Chicago (USA), pages 39–42, 2000.

    Google Scholar 

  36. Ch. Meinel and A. Wagner, WWW.BDD-Portal.Org-An Electronic Basis for Cooperative Research in EDA, Proc. CRIS 2000, Espoo, Helsinki, Finnland, USA, 2000.

    Google Scholar 

  37. R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. IEEE International Conference on Computer-Aided Design (Santa Clara,CA), pages 42–47, 1993.

    Google Scholar 

  38. H. Sack, E. Dubrova, Ch. Meinel Mod-p Decision Diagrams: A Data-Structure for Multiple-Valued Functions, in Proc. of the 2000 IEEE/ACM Int. Workshop on Logic Synthesis (IWLS2000), 2000.

    Google Scholar 

  39. D. Sieling, On the Existence of Polynomial Time Approximation Schemes for OBDD Minimization. in Proc. of Symposium on theoretical aspects in Computer Science, pages 205–215, 1998.

    Google Scholar 

  40. A. Slobodová and C. Meinel, Sample Method for Minimization of OBDDs. In Proc. of the International Workshop on Logic Synthesis, pages 311–316, 1998.

    Google Scholar 

  41. S. Tani, K. Hamaguchi, and S. Yajima. The complexity of the optimal variable ordering problems of shared binary decision diagrams. In Proc. International Symposium on Algorithms and Computation’ 93, volume 762 of Lecture Notes in Computer Science, pages 389–398. Springer, 1993.

    Google Scholar 

  42. S. Waack, On the descriptive and algorithmic power of parity ordered binary decision diagrams, Proc. 14th Symp. on Theoretical Aspects of Computer Science, 1200 of LNCS, Springer, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB IV - Informatik, Universität Trier, 54286, Trier, Germany

    Christoph Meinel & Christian Stangier

Authors
  1. Christoph Meinel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Stangier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Freie Universität Berlin, Takustr. 9, 14195, Berlin, Germany

    Helmut Alt

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Meinel, C., Stangier, C. (2001). Data Structures for Boolean Functions BDDs — Foundations and Applications. In: Alt, H. (eds) Computational Discrete Mathematics. Lecture Notes in Computer Science, vol 2122. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45506-X_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-45506-X_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42775-9

  • Online ISBN: 978-3-540-45506-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation