Article

Free access

Verification of arithmetic circuits with binary moment diagrams

Authors:

Randal E. Bryant,

Yirng-An ChenAuthors Info & Claims

DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation Conference

Pages 535 - 541

https://doi.org/10.1145/217474.217583

Published: 01 January 1995 Publication History

PDF eReader

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," International Conference on Computer- Aided Design, November, 1993, pp. 188-191.

Digital Library

Google Scholar

[2]

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

Digital Library

Google Scholar

[3]

R. E. Bryant, and Y.-A. Chen, "Verification of arithmetic functions with binary moment diagrams," Technical Report CMU- CS-94-160, Carnegie Mellon University, May, 1994.

Digital Library

Google Scholar

[4]

J. R. Burch, "Using BDDs to verify multipliers," 28th Design Automation Conference, June, 1991, pp. 408-412.

Digital Library

Google Scholar

[5]

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 ACM/IEEE Design Automation Conference, Dallas, TX, June, 1993, pp. 54-60.

Digital Library

Google Scholar

[6]

R. Enders, "Note on the complexity of binary moment diagram representations," unpublished paper, Siemens AG, Munich Germany, 1994.

Google Scholar

[7]

J. Jain, J. Bitner, M. Abadir, J. A. Abraham, and D. S. Fussell, "Indexed BDDs: Algorithmic advances in techniques to represent and verify Boolean functions," submitted for publication, 1994.

Google Scholar

[8]

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

Google Scholar

[9]

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

Google Scholar

[10]

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

Digital Library

Google Scholar

[11]

S.-i. Minato, "Implicit manipulation of polynomials using zerosuppressed BDDs," unpublished manuscript, 1994.

Google Scholar

[12]

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

Google Scholar

Cited By

View all

Sistla MChaudhuri SReps T(2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689760
Sistla MChaudhuri SReps T(2024)CFLOBDDs: Context-Free-Language Ordered Binary Decision DiagramsACM Transactions on Programming Languages and Systems10.1145/365115746:2(1-82)Online publication date: 2-May-2024
https://dl.acm.org/doi/10.1145/3651157
Kleinekathöfer JMahzoon ADrechsler R(2023)Polynomial Formal Verification of Floating Point Adders2023 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE56975.2023.10137166(1-2)Online publication date: Apr-2023
https://doi.org/10.23919/DATE56975.2023.10137166
Show More Cited By

Index Terms

Verification of arithmetic circuits with binary moment diagrams
1. Hardware

Recommendations

Efficient construction of binary moment diagrams for verifying arithmetic circuits
ICCAD '95: Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design

BDD-based approaches cannot handle some arithmetic functions such as multiplication efficiently, while Binary Moment Diagrams proposed by Bryant and Chen provide compact representations for those functions. They reported a BMD-based polynomial-time ...
Formal Verification of Arithmetic Circuits by Function Extraction

This paper presents an algebraic approach to functional verification of gate-level, integer arithmetic circuits. It is based on extracting a unique bit-level polynomial function computed by the circuit directly from its gate-level implementation. The ...
Verification of Arithmetic Functions with Binary Moment Diagrams

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation Conference

January 1995

760 pages

ISBN:0897917251

DOI:10.1145/217474

Chairman:
Bryan T. Preas
Xerox Parc, Palo Alto, CA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1995

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

DAC95

Sponsor:

EDAC
SIGDA

DAC95: The 32nd Design Automation Conference

June 12 - 16, 1995

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

240
Total Citations
View Citations
665
Total Downloads

Downloads (Last 12 months)95
Downloads (Last 6 weeks)16

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sistla MChaudhuri SReps T(2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689760
Sistla MChaudhuri SReps T(2024)CFLOBDDs: Context-Free-Language Ordered Binary Decision DiagramsACM Transactions on Programming Languages and Systems10.1145/365115746:2(1-82)Online publication date: 2-May-2024
https://dl.acm.org/doi/10.1145/3651157
Kleinekathöfer JMahzoon ADrechsler R(2023)Polynomial Formal Verification of Floating Point Adders2023 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE56975.2023.10137166(1-2)Online publication date: Apr-2023
https://doi.org/10.23919/DATE56975.2023.10137166
Kumar JMiyasaka YSrivastava AFujita M(2023)Formal Verification of Integer Multiplier Circuits Using Binary Decision DiagramsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.319217642:4(1365-1378)Online publication date: Apr-2023
https://doi.org/10.1109/TCAD.2022.3192176
Zulehner AWille RZulehner AWille R(2023)Effiziente Implementierung von DDs im QuantenbereichEinführung in die Entwurfsautomatisierung für Quantencomputer10.1007/978-3-031-36751-9_7(73-84)Online publication date: 15-Dec-2023
https://doi.org/10.1007/978-3-031-36751-9_7
Zulehner AWille RZulehner AWille R(2023)Entwurfsautomatisierungsmethoden für konventionelle SystemeEinführung in die Entwurfsautomatisierung für Quantencomputer10.1007/978-3-031-36751-9_3(23-28)Online publication date: 15-Dec-2023
https://doi.org/10.1007/978-3-031-36751-9_3
Kaufmann D(2022)Formal verification of multiplier circuits using computer algebrait - Information Technology10.1515/itit-2022-003964:6(285-291)Online publication date: 24-Jun-2022
https://doi.org/10.1515/itit-2022-0039
Hong XZhou XLi SFeng YYing M(2022)A Tensor Network based Decision Diagram for Representation of Quantum CircuitsACM Transactions on Design Automation of Electronic Systems10.1145/351435527:6(1-30)Online publication date: 27-Jun-2022
https://dl.acm.org/doi/10.1145/3514355
Drechsler RMahzoon AMitra TYoung EXiong J(2022)Polynomial Formal VerificationProceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design10.1145/3508352.3561104(1-9)Online publication date: 30-Oct-2022
https://dl.acm.org/doi/10.1145/3508352.3561104
Ito AUeno RHomma N(2022)Efficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean PolynomialsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.305992441:3(794-798)Online publication date: Mar-2022
https://doi.org/10.1109/TCAD.2021.3059924
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

Efficient construction of binary moment diagrams for verifying arithmetic circuits

Formal Verification of Arithmetic Circuits by Function Extraction

Verification of Arithmetic Functions with Binary Moment Diagrams