Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Techniques for Smaller Intermediary BDDs

  • Conference paper
  • First Online:
CONCUR 2001 — Concurrency Theory (CONCUR 2001)

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

Included in the following conference series:

Abstract

Binary decision diagrams (BDDs) have proven to be a powerful technique for combating the state explosion problem. Their application to verification is usually centered around the computation of the transitive closure of some binary relation. The closure is usually computed with a fixed point algorithm that expands some set until it stops growing. Unfortunately, the BDDs that arise during the computation are often much larger than the final BDD. The computation may thus fail because of lack of memory, even if the final BDD would be small. To alleviate this problem, this paper proposes four variations of the fixed point algorithm. They reduce the sizes of the intermediary BDDs by “rounding down” the sets they represent in such a way that the final BDD does not change. Consequently, more iterations may be required to compute the fixed point, but the intermediary BDDs computed during the run are smaller. The performance of the new algorithms is illustrated with a large number of experiments.

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. R. Alur, R.K. Brayton, T. Henzinger, S. Qadeer, & S.K. Rajamani. Partial-order reduction in symbolic state space exploration. In CAV’97: Proc. 9th Intl. Conf. Computer-Aided Verification, LNCS #1254, pp. 340–351. Springer-Verlag, Jun 1997.

    Google Scholar 

  2. R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, & F. Somenzi. Algebraic decision diagrams and their applications. In Proc. ACM/IEEE Intl. Conf. Computer-Aided Design, pp. 188–191, Nov 1993.

    Google Scholar 

  3. A. Biere, A. Cimatti, E.M. Clarke, & Y. Zhu. Symbolic model checking without BDDs. In Proc. 5th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems, LNCS #1579, pp. 193–207. Springer-Verlag, Mar 1999.

    Chapter  Google Scholar 

  4. R. Bloem, I.-H. Moon, K. Ravi, & F. Somenzi. Approximations for fixpoint computations in symbolic model checking. In Proc. World Multiconference on Systemics, Cybernetics and Informatics, Vol. VIII, Part II, pp. 701–706, 2000.

    Google Scholar 

  5. R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, C-35(8):677–691, Aug 1986.

    Google Scholar 

  6. J.R. Burch, E.M. Clarke, & D.E. Long. Symbolic model checking with partitioned transition relations. In Proc. IFIP Intl. Conf. Very Large Scale Integration, pp. 49–58, Aug 1991.

    Google Scholar 

  7. J.R. Burch, E.M. Clarke, D.E. Long, K.L. MacMillan, & D.L. Dill. Symbolic model checking for sequential circuit verification. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 13(4):401–424, Apr 1994.

    Google Scholar 

  8. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, & L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, Jun 1992.

    Google Scholar 

  9. G. Cabodi, P. Camurati, L. Lavagno, & S. Quer. Disjunctive partitioning and partial iterative squaring: An effective approach for symbolic traversal of large circuits. In Proc. 34th ACM/IEEE Conf. Design Automation, pp. 728–733, Jun 1997.

    Google Scholar 

  10. G. Cabodi, P. Camurati, & S. Quer. Improved reachability analysis of large finite state machines. In Proc. ACM/IEEE Intl. Conf. Computer-Aided Design, pp. 354–360, Nov 1996.

    Google Scholar 

  11. G. Cabodi, P. Camurati, & S. Quer. Improving symbolic traversals by means of activity profiles. In Proc. 36th ACM/IEEE Conf. Design Automation, pp. 306–311, Jun 1999.

    Google Scholar 

  12. H. Cho, G.D. Hachtel, E. Macii, B. Plessier, & F. Somenzi. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 15(12):1451–1464, Dec 1996.

    Google Scholar 

  13. H. Cho, G.D. Hachtel, E. Macii, B. Plessier, & F. Somenzi. Algorithms for approximate FSM traversal based on state space decomposition. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 15(12):1465–1478, Dec 1996.

    Google Scholar 

  14. O. Coudert, C. Berthet, & J.C. Madre. Verification of synchronous sequential machines based on symbolic execution. In Proc. Intl. Workshop on Automatic Verification Methods for Finite State Systems, LNCS #407, pp. 365–373. Springer-Verlag, Jun 1989.

    Google Scholar 

  15. M. Fujita, Y. Matsunaga, & T. Kakuda. On variable ordering of binary decision diagrams for the application of multi-level logic synthesis. In Proc. European Design Automation Conference, pp. 50–54, 1991.

    Google Scholar 

  16. S.G. Govindaraju, D.L. Dill, A.J. Hu, & M.A. Horowitz. Approximate reachability with BDDs using overlapping projections. In Proc. 35th ACM/IEEE Conf. Design Automation, pp. 451–456, Jun 1998.

    Google Scholar 

  17. A.J. Hu. Efficient Techniques for Formal Verification Using Binary Decision Diagrams. PhD thesis, Stanford Univ., 1995.

    Google Scholar 

  18. A.J. Hu, G. York, & D.L. Dill. New techniques for efficient verification with implicitly conjoined BDDs. In Proc. 31th ACM/IEEE Conf. Design Automation, pp. 276–282, Jun 1994.

    Google Scholar 

  19. S.-i. Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In Proc. 30th ACM/IEEE Conf. Design Automation, pp. 272–277, Jun 1993.

    Google Scholar 

  20. T. Kam. State Minimization of Finite State Machines using Implicit Techniques. PhD thesis, Electronics Research Laboratory, Univ. of California at Berkeley, 1995.

    Google Scholar 

  21. R.P. Kurshan. Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, 1994.

    Google Scholar 

  22. D.E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, Carnegie-Mellon Univ., 1993.

    Google Scholar 

  23. A. Miner & G. Ciardo. Efficient reachability set generation and storage using decision diagrams. In Proc. 20th Intl. Conf. Application and Theory of Petri Nets, LNCS #1639, pp. 6–25. Springer-Verlag, Jun 1999.

    Google Scholar 

  24. A. Narayan, A.J. Isles, J. Jain, R.K. Brayton, & A.L. Sangiovanni-Vincentelli. Reachability analysis using partitioned-ROBDDs. In Proc. ACM/IEEE Intl. Conf. Computer-Aided Design, pp. 388–393, Nov 1997.

    Google Scholar 

  25. E. Pastor, O. Roig, J. Cortadella, & R. Badia. Petri net analysis using boolean manipulation. In Proc. 15th Intl. Conf. Application and Theory of Petri Nets, LNCS #815, pp. 416–435. Springer-Verlag, 1994.

    Google Scholar 

  26. K. Ravi & F. Somenzi. High-density reachability analysis. In Proc. ACM/IEEE Intl. Conf. Computer-Aided Design, pp. 154–158, Nov 1995.

    Google Scholar 

  27. K. Ravi & F. Somenzi. Hints to accelerate symbolic traversal. In Proc. 10th IFIP WG 10.5 Intl. Conf. Correct Hardware Design and Verification Methods, LNCS #1703, pp. 250–264. Springer-Verlag, Sept 1999.

    Google Scholar 

  28. R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. ACM/IEEE Intl. Conf. Computer-Aided Design, pp. 42–47, Nov 1993.

    Google Scholar 

  29. A. Srinivasan, T. Kam, S. Malik, & R.K. Brayton. Algorithms for discrete function manipulation. In Proc. ACM/IEEE Intl. Conf. Computer-Aided Design, pp. 92–97, Nov 1990.

    Google Scholar 

  30. S. Waack. On the descriptive and algorithmic power of parity ordered binary decision diagrams. In Proc. 14th Annual Symposium on Theoretical Aspects of Computer Science, LNCS #1200, pp. 201–212. Springer-Verlag, Feb 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Systems Laboratory, Tampere University of Technology, PO Box 553, FIN-33101, Tampere, Finland

    Jaco Geldenhuys & Antti Valmari

Authors
  1. Jaco Geldenhuys
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antti Valmari
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, BRICS, Aalborg University, Fredrik Bajersvej 7, 9220, Aalborg, Denmark

    Kim G. Larsen

  2. BRICS, Aarhus University, Ny Munkegade, Bldg. 540, 8000, Aarhus C, Denmark

    Mogens Nielsen

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Geldenhuys, J., Valmari, A. (2001). Techniques for Smaller Intermediary BDDs. In: Larsen, K.G., Nielsen, M. (eds) CONCUR 2001 — Concurrency Theory. CONCUR 2001. Lecture Notes in Computer Science, vol 2154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44685-0_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-44685-0_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42497-0

  • Online ISBN: 978-3-540-44685-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation