Article

Free access

Hybrid decision diagrams

Authors:

E. M. Clarke,

M. Fujita,

X. ZhaoAuthors Info & Claims

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

Pages 159 - 163

Published: 01 December 1995 Publication History

PDF eReader Publisher Site

Abstract

Abstract: Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. We show how to implement arithmetic operations efficiently for hybrid decision diagrams. In practice, this is one of the main limitations of BMDs since performing arithmetic operations on functions expressed in this notation can be very expensive. In order to extend symbolic model checking algorithms to handle arithmetic properties, it is essential to be able to compute the BDD for the set of variable assignments that satisfy an arithmetic relation. In our paper, we give an efficient algorithm for this purpose. Moreover, we prove that for the class of linear expressions, the time complexity of our algorithm is linear in the number of variables.

References

[1]

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. In Proceedings of the 1993 IEEE International Conference on Computer Aided Design. IEEE Computer Society Press, November 1993.

Digital Library

Google Scholar

[2]

R. Bellman. Introcution to matrix analysis, chapter 5. McGraw-Hill, 1970.

Digital Library

Google Scholar

[3]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.

Digital Library

Google Scholar

[4]

R. E. Bryant and Y. A. Chert. Verification of arithmetic functions with binary moment diagrams. In Proceedings of the 32nd A CM/IEEE Design Automation Conference. IEEE Computer Society Press, June 1995.

Digital Library

Google Scholar

[5]

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 102o states and beyond. Information and Computation, 98(2):142- 170, June 1992.

Digital Library

Google Scholar

[6]

E. M. Clarke, K. McMillan, X. Zhao, M. Fujita, and J. Yang. Spectral transforms for large boolean functions with applications to technology mapping. In Proceedings of the 30th A CM/IEEE Design Automation Conference. IEEE Computer Society Press, June 1993.

Digital Library

Google Scholar

[7]

R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M. A. Perkowski. Efficient representation and manipulation of switching functions based on ordered kroenecker functional decision diagrams. In Proceedings of the 32nd A CM/IEEE Design Automation Conference. IEEE Computer Society Press, June 1994.

Digital Library

Google Scholar

[8]

R. Drechsler, M. Theobald, and B. Becker. Fast ofdd based minimization of fixed polarity reed-muller expressions. In Proceedings of the 1994 European Design Automation Conference. IEEE Computer Society Press, June 1994.

Digital Library

Google Scholar

[9]

D. E. Muller. Application of boolean algebra to switching circuit design and error detection. IRE Trans, 1:6-12, 1954.

Google Scholar

Cited By

View all

Vasudevan SViswanath VSumners RAbraham J(2007)Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting SystemsIEEE Transactions on Computers10.1109/TC.2007.107356:10(1401-1414)Online publication date: 1-Oct-2007
https://dl.acm.org/doi/10.1109/TC.2007.1073
Jerinić VLanger JHeinkel UMüller DGielen G(2006)New methods and coverage metrics for functional verificationProceedings of the conference on Design, automation and test in Europe: Proceedings10.5555/1131481.1131764(1025-1030)Online publication date: 6-Mar-2006
https://dl.acm.org/doi/10.5555/1131481.1131764
Kruger LJha SGoh EBoneh DJuels AWright RDe Capitani di Vimercati S(2006)Secure function evaluation with ordered binary decision diagramsProceedings of the 13th ACM conference on Computer and communications security10.1145/1180405.1180455(410-420)Online publication date: 30-Oct-2006
https://dl.acm.org/doi/10.1145/1180405.1180455
Show More Cited By

Index Terms

Hybrid decision diagrams
1. Hardware
  1. Hardware validation

Recommendations

Bit-Serial Systolic Divider and Multiplier for Finite Fields GF(2/sup m/)
Special issue on computer arithmetic

A systolic structure for bit-serial division over the field GF(2/sup m/) is developed. Consideration is given to avoid global data communications and dependency of the time step duration on m. This is important for applications where the value of m is ...
A VLSI Modulo m Multiplier

A novel method to compute the exact digits of the modulo m product of integers is proposed, and a modulo m multiply structure is defined. Such a structure can be implemented by means of a few fast VLSI binary multipliers, and a response time of about ...
Comments on "A Characterization of Binary Decision Diagrams"

Chakravarty presents a characterization of BDD's in terms of the complexity of some computational problems. In these comments, some incorrectly stated restrictions on the "number of repeated variables" are corrected and results on the translation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

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

Publisher

IEEE Computer Society

United States

Publication History

Published: 01 December 1995

Check for updates

Author Tags

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

25
Total Citations
View Citations
299
Total Downloads

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

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Vasudevan SViswanath VSumners RAbraham J(2007)Automatic Verification of Arithmetic Circuits in RTL Using Stepwise Refinement of Term Rewriting SystemsIEEE Transactions on Computers10.1109/TC.2007.107356:10(1401-1414)Online publication date: 1-Oct-2007
https://dl.acm.org/doi/10.1109/TC.2007.1073
Jerinić VLanger JHeinkel UMüller DGielen G(2006)New methods and coverage metrics for functional verificationProceedings of the conference on Design, automation and test in Europe: Proceedings10.5555/1131481.1131764(1025-1030)Online publication date: 6-Mar-2006
https://dl.acm.org/doi/10.5555/1131481.1131764
Kruger LJha SGoh EBoneh DJuels AWright RDe Capitani di Vimercati S(2006)Secure function evaluation with ordered binary decision diagramsProceedings of the 13th ACM conference on Computer and communications security10.1145/1180405.1180455(410-420)Online publication date: 30-Oct-2006
https://dl.acm.org/doi/10.1145/1180405.1180455
Lotfi-Kamran PHosseinabady MShojaei HMassoumi MNavabi ZTang T(2005)TED+Proceedings of the 2005 Asia and South Pacific Design Automation Conference10.1145/1120725.1120964(567-572)Online publication date: 18-Jan-2005
https://dl.acm.org/doi/10.1145/1120725.1120964
Bartzis CBultan T(2003)Construction of efficient BDDs for bounded arithmetic constraintsProceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems10.5555/1765871.1765908(394-408)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1765871.1765908
Keim MDrechsler RBecker BMartin MMolitor P(2003)Polynomial Formal Verification of MultipliersFormal Methods in System Design10.1023/A:102175213039422:1(39-58)Online publication date: 1-Jan-2003
https://dl.acm.org/doi/10.1023/A%3A1021752130394
Scholl CBecker BWeis T(2002)On WLCDs and the Complexity of Word-Level Decision Diagrams—A Lower Bound for DivisionFormal Methods in System Design10.1023/A:101470233182820:3(311-326)Online publication date: 1-May-2002
https://dl.acm.org/doi/10.1023/A%3A1014702331828
Clarke ESchlingloff B(2001)Model checkingHandbook of automated reasoning10.5555/778522.778533(1635-1790)Online publication date: 1-Jan-2001
https://dl.acm.org/doi/10.5555/778522.778533
Thornton MDrechsler R(2001)Spectral decision diagrams using graph transformationsProceedings of the conference on Design, automation and test in Europe10.5555/367072.367860(713-719)Online publication date: 13-Mar-2001
https://dl.acm.org/doi/10.5555/367072.367860
(2000)Efficient Dynamic Minimization of Word-Level DDs Based on Lower Bound ComputationProceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors10.5555/557517.846829Online publication date: 17-Sep-2000
https://dl.acm.org/doi/10.5555/557517.846829
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Cited By

Index Terms

Recommendations

Bit-Serial Systolic Divider and Multiplier for Finite Fields GF(2/sup m/)

A VLSI Modulo m Multiplier

Comments on "A Characterization of Binary Decision Diagrams"