Article

Free access

Binary decision diagrams and beyond: enabling technologies for formal verification

Author:

Randal E. BryantAuthors Info & Claims

ICCAD '95: Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design

Pages 236 - 243

Published: 01 December 1995 Publication History

PDF eReader Publisher Site

Abstract

Ordered Binary Decision Diagrams (OBDDs) have found widespread use in CAD applications such as formal verification, logic synthesis, and test generation. OBDDs represent Boolean functions in a form that is both canonical and compact for many practical cases. They can be generated and manipulated by efficient graph algorithms. Researchers have found that many tasks can be expressed as series of operations on Boolean functions, making them candidates for OBDD-based methods. The success of OBDDs has inspired efforts to improve their efficiency and to expand their range of applicability. Techniques have been discovered to make the representation more compact and to represent other classes of functions. This has led to improved performance on existing OBDD applications, as well as enabled new classes of problems to be solved. This paper provides an overview of the state of the art in graph-based function representations. We focus on several recent advances of particular importance for formal verification and other CAD applications.

References

[1]

S.B. Akers, "Binary decision diagrams," IEEE Transactions on Computers, Vol. C-27, No. 6 (June, 1978), pp. 509-516.

[2]

E Ashar, S. Devadas, and A. Ghosh, "Boolean satisfiability and equivalence checking using general binary decision diagrams," International Conference on Computer Design, IEEE, 1991, pp. 259-264.

Digital Library

[3]

R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel, E. Macii, A. Pardo, and F .Somenzi, "Algebraic decision diagrams and their applications," International Conference on Computer-Aided Design, November, 1993, pp. 188-191.

Digital Library

[4]

J. Bern, C. Meinel, and A. Slobodov{t, "Efficient OBDD- based Boolean manipulation in CAD beyond current limits," 32nd Design Automation Conference, June, 1995, pp. 408- 413.

Digital Library

[5]

K. S. Brace, R. L. Rudell, and R. E. Bryant, "Efficient implementation of a BDD package," 27th Design Automation Conference, June, 1990, pp. 40-45.

Digital Library

[6]

R.E. Bryant, "Graph-basedalgorithms for Boolean function manipulation," IEEE Transactions on Computers, Vol. C- 35, No. 8 (August, 1986), pp. 677-691.

Digital Library

[7]

R.E. Bryant, "On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication," IEEE Transactions on Computers, Vol. 40, No. 2 (February, 1991), pp. 205-213.

Digital Library

[8]

R. E. Bryant, "Symbolic Boolean manipulation with ordered binary decision diagrams," ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.

Digital Library

[9]

R. E. Bryant, and Y.-A. Chen, "Verification of arithmetic circuits with binary moment diagrams," 32nd Design Automation Conference, June, 1995, pp. 535-541.

Digital Library

[10]

E. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. C.-Y. Yang, "Spectral transforms for large Boolean functions with application to technology mapping," 30th Design Automation Conference, June, 1993, pp. 54-60.

Digital Library

[11]

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.

Digital Library

[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," 31st Design Automation Conference, June, 1994, pp. 415-419.

Digital Library

[13]

M. Fujita, H. Fujisawa, and N. Kawato, "Evaluations and improvements of a Boolean comparison program based on binary decision diagrams," International Conference on Computer-Aided Design, November, 1988, pp. 2-5.

[14]

J. Gergov, C. Meinel, "Efficient Boolean Manipulation with OBDDs can be extended to FBDDs," IEEE Transactions on Computers, Vol. 43, No. 10 (October, 1994), pp. 1197-1209.

Digital Library

[15]

K. Hamaguchi, A. Morita, and S. Yajima, "Efficient construction of binary moment diagrams for verifying arithmetic circuits," International Conference on Computer- Aided Design, November, 1995.

Digital Library

[16]

U. Kebschull, E. Schubert, and W. Rosentiel, "Multilevel logic based on functional decision diagrams," European Design Automation Conference, 1992, pp. 43-47.

[17]

Y.-T. Lai, and S. Sastry, "Edge-valued binary decision diagrams for multi-level hierarchical verification," 29th Design Automation Conference, June, 1992, pp. 608-613.

Digital Library

[18]

Y.-T. Lai, M. Pedram, and S. B. K. Vrudhula, "EVBDD- based algorithms for integer linear programming, spectral transformation, and function decomposition," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 13, No. 8 (August, 1994), pp. 959-975.

Digital Library

[19]

S. Malik, A. Wang, R. K. Brayton, and A. Sangiovanni- Vincentelli, "Logic verification using binary decision diagrams in a logic synthesis environment," International Conference on Computer-Aided Design, November, 1988, pp. 6-9.

[20]

S.-i. Minato, "Zero-suppressed BDDs for set manipulation in combinatorial problems," 30th Design Automation Conference, June, 1993, pp. 272-277.

Digital Library

[21]

S.-i. Minato, Binary Decision Diagrams and Applications for VLSI CAD, Kluwer, 1995.

Digital Library

[22]

H. Ochi, K. Yasuoka, and S. Yajima, "Breadth-first manipulation of very large binary-decision diagrams," International Conference on Computer-Aided Design, November, 1993, pp. 48-55.

Digital Library

[23]

S. Ponzio, "A lower bound for integer multiplication with read-once only branching programs," Symposium on Theory of Computing, ACM, 1995.

Digital Library

[24]

O. SchriSer, and I. Wegener, "The theory of zero-suppressed BDDs and the number of knights tours," Technical report 552/1994, University of Dortmund, Fachbereich Informatik, 1994.

[25]

D. Sieling, and I. Wegener, "Graph-driven OBDDs--a new data structure for Boolean functions," Theoretical Computer Science, 1995.

Digital Library

[26]

R. Rudell, "Dynamic variable ordering for ordered binary decision diagrams," International Conference on Computer- Aided Design, November, 1993, pp. 42-47.

Digital Library

Cited By

Nath RDas SSural SVaidya JAtluri VKerschbaum FMashatan ANiu JLee A(2019)PolTreeProceedings of the 24th ACM Symposium on Access Control Models and Technologies10.1145/3322431.3325102(25-35)Online publication date: 28-May-2019
https://dl.acm.org/doi/10.1145/3322431.3325102
Chandrasekharan AGroße DDrechsler RTalpin JDerler PSchneider K(2017)Yise - a novel framework for boolean networks using y-inverter graphsProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3127041.3127065(114-117)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3127041.3127065
Shirinzadeh SSoeken MGroße DDrechsler RBosman P(2017)An adaptive prioritized ε-preferred evolutionary algorithm for approximate BDD optimizationProceedings of the Genetic and Evolutionary Computation Conference10.1145/3071178.3071281(1232-1239)Online publication date: 1-Jul-2017
https://dl.acm.org/doi/10.1145/3071178.3071281
Show More Cited By

Index Terms

Binary decision diagrams and beyond: enabling technologies for formal verification
1. Hardware
  1. Hardware validation
    1. Functional verification
2. Mathematics of computing
  1. Discrete mathematics

Recommendations

Bddl: A Type System for Binary Decision Diagrams
Tests and Proofs
Abstract
Binary Decision Diagrams (BDDs) are compact data structures used to efficiently store and process boolean functions. BDDs have many uses, from system design to model checking to efficiently storing context information for context-sensitive ...
Data decision diagrams for Promela systems analysis

In this paper, we show how to verify computation tree logic (CTL) properties, using symbolic methods, on systems described in Promela. Symbolic representation is based on data decision diagrams (DDDs) which are n-valued Shared Decision Trees designed to ...
Beyond lassos: complete SMT-Based bounded model checking for timed automata
FMOODS'12/FORTE'12: Proceedings of the 14th joint IFIP WG 6.1 international conference and Proceedings of the 32nd IFIP WG 6.1 international conference on Formal Techniques for Distributed Systems

Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. Previous SMT-based BMC approaches for TAs search for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '95: Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design

December 1995

748 pages

ISBN:0818672137

Chairman:
Richard Rudell
Synopsys, Inc., Mountain View, CA

Copyright © Copyright (c) 1995 Institute of Electrical and Electronics Engineers, Inc. All rights reserved.

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS: Computer Society

Publisher

IEEE Computer Society

United States

Publication History

Published: 01 December 1995

Check for updates

Qualifiers

Article

Conference

ICCAD '95

Sponsor:

SIGDA
IEEE-CS

ICCAD '95: International Conference on Computer Aided Design

November 5 - 9, 1995

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

48
Total Citations
View Citations
654
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)4

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nath RDas SSural SVaidya JAtluri VKerschbaum FMashatan ANiu JLee A(2019)PolTreeProceedings of the 24th ACM Symposium on Access Control Models and Technologies10.1145/3322431.3325102(25-35)Online publication date: 28-May-2019
https://dl.acm.org/doi/10.1145/3322431.3325102
Chandrasekharan AGroße DDrechsler RTalpin JDerler PSchneider K(2017)Yise - a novel framework for boolean networks using y-inverter graphsProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3127041.3127065(114-117)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3127041.3127065
Shirinzadeh SSoeken MGroße DDrechsler RBosman P(2017)An adaptive prioritized ε-preferred evolutionary algorithm for approximate BDD optimizationProceedings of the Genetic and Evolutionary Computation Conference10.1145/3071178.3071281(1232-1239)Online publication date: 1-Jul-2017
https://dl.acm.org/doi/10.1145/3071178.3071281
Shirinzadeh SSoeken MGroße DDrechsler RNeumann FSutton A(2016)Approximate BDD Optimization with Prioritized ε-Preferred Evolutionary AlgorithmProceedings of the 2016 on Genetic and Evolutionary Computation Conference Companion10.1145/2908961.2908987(79-80)Online publication date: 20-Jul-2016
https://dl.acm.org/doi/10.1145/2908961.2908987
Weiss CRubio-González CLiblit BBertolino ACanfora GElbaum S(2015)Database-backed program analysis for scalable error propagationProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818827(586-597)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2818754.2818827
Shirinzadeh SSoeken MDrechsler REsparcia-Alcázar A(2015)Multi-Objective BDD Optimization with Evolutionary AlgorithmsProceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation10.1145/2739480.2754718(751-758)Online publication date: 11-Jul-2015
https://dl.acm.org/doi/10.1145/2739480.2754718
Tarau PChitil OKing ADanvy O(2014)Bijective Collection Encodings and Boolean Operations with Hereditarily Binary Natural NumbersProceedings of the 16th International Symposium on Principles and Practice of Declarative Programming10.1145/2643135.2643139(31-42)Online publication date: 8-Sep-2014
https://dl.acm.org/doi/10.1145/2643135.2643139
Khmelevsky YRinard MSidiroglou-Douskos SNg JCordy JCzarnecki K(2013)A source-to-source transformation tool for error fixingProceedings of the 2013 Conference of the Center for Advanced Studies on Collaborative Research10.5555/2555523.2555540(147-160)Online publication date: 18-Nov-2013
https://dl.acm.org/doi/10.5555/2555523.2555540
Schneider DTrapp M(2013)Conditional Safety Certification of Open Adaptive SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/2491465.24914678:2(1-20)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1145/2491465.2491467
Liu XTan SWang HRosenstiel WMacii E(2012)Parallel statistical analysis of analog circuits by GPU-accelerated graph-based approachProceedings of the Conference on Design, Automation and Test in Europe10.5555/2492708.2492920(852-857)Online publication date: 12-Mar-2012
https://dl.acm.org/doi/10.5555/2492708.2492920
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents