Article

Free access

A decision procedure for bit-vector arithmetic

Authors:

Clark W. Barrett,

David L. Dill,

Jeremy R. LevittAuthors Info & Claims

DAC '98: Proceedings of the 35th annual Design Automation Conference

Pages 522 - 527

https://doi.org/10.1145/277044.277186

Published: 01 May 1998 Publication History

PDF eReader

Abstract

Bit-v ector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in suc h a theory is NP-hard, our implementation is efficient for many practical examples. We believ e this to be the first such implementation which is efficient, automatic, and complete.

References

[1]

LaurentArditi. *BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions. In Srivas {12}, pages 34-48.

Digital Library

Google Scholar

[2]

C. W. Barrett, D. L. Dill, and J. R. Levitt. Validity Checking for Combinations of Theories with Equality. In Srivas {12}, pages 187-201.

Digital Library

Google Scholar

[3]

Randal E. Bryant and Yirng-An Chen. Verification of Arithmetic Circuits with Binary Moment Diagrams. In 32~d ACM/IEEE Design Automation Conference, pages 535-541, San Francisco, CA (USA), 1995.

Digital Library

Google Scholar

[4]

J R. Burch and D. L. Dill. Automatic Verification of Microprocessor Control. In Dill, editor, Computer- Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 68-79, Stanford, CA (USA), June 1994.

Digital Library

Google Scholar

[5]

D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak's Decision Procedure for Combinations of Theories. In 13th International Conference on Automated Deduction, pages 463-477, Rutgers University, NJ (USA), July 1996.

Digital Library

Google Scholar

[6]

D. Cyrluk, 0. MSller, and H. Ruefi. An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors. In 9thInternational Conference on Computer- Aided Verification, 1997.

Digital Library

Google Scholar

[7]

Joseph A. Gallian. Contemporary Abstract Algebra. D. C. Heath and Company, second edition, 1990.

Google Scholar

[8]

Warren A. Hunt Jr. Microprocessor Design Verification. Journal of Automated Reasoning, 5(4), December 1989.

Digital Library

Google Scholar

[9]

R. B. Jones, D. L. Dill, and J. R. Butch. Efficient Validity Checking for Processor Verification. In IEEE Internationl Conference on Computer-Aided Design, pages 2-6, San Jose, CA (USA), November 1995. ~ Computer Society Press.

Digital Library

Google Scholar

[10]

Leo G. Marcus. SOVS 13 Users'Manual. The Aerospace Corporation, E1 Segundo, CA 90245, October 1994. Aerospace Report ATR-94(4778)-5.

Google Scholar

[11]

M. Smith, M. Lain, and M. Horowitz. Boosting Beyond Static Scheduling in a Superscalar Processor. In International Symposium on Computer Architecture, pages 344-354, Seattle, WA, May 1990. IEEF} ACM.

Digital Library

Google Scholar

[12]

Srivas, editor. International Conference on Formal Methods in Computer-Aided Design, volume 818 of Lecture Notes in Computer Science, Palo Alto, CA (USA), November 1996. Springer-Verlag.

Digital Library

Google Scholar

[13]

Wai Wong. Modelling Bit Vectors in HOL: the word Library. In Joyce and Seger, editors, Higher Order Logic Theorem Proving and Its Applications, volume 780 of Lecture Notes in Computer Science, pages 371- 384, Vancouver, Canada, August 1993.

Digital Library

Google Scholar

Cited By

View all

Fan HHe F(2024)Leveraging Datapath Propagation in IC3 for Hardware Model CheckingIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.336002243:7(2215-2228)Online publication date: Jul-2024
https://doi.org/10.1109/TCAD.2024.3360022
Faure-Gignoux ADelmas KGauffriau APagetti C(2024)Methodology for Formal Verification of Hardware Safety Strategies Using SMTIEEE Embedded Systems Letters10.1109/LES.2024.343985916:4(381-384)Online publication date: Dec-2024
https://doi.org/10.1109/LES.2024.3439859
Trabish DItzhaky SRinetzky NSpinellis DGousios GChechik MDi Penta M(2021)A bounded symbolic-size model for symbolic executionProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3468264.3468596(1190-1201)Online publication date: 20-Aug-2021
https://dl.acm.org/doi/10.1145/3468264.3468596
Show More Cited By

Index Terms

A decision procedure for bit-vector arithmetic

Recommendations

A fast bit-vector algorithm for approximate string matching based on dynamic programming

The approximate string matching problem is to find all locations at which a query of lengthm matches a substring of a text of length n with k-or-fewer differences. Simple and practical bit-vector algorithms have been designed for this problem, most ...
egg: Fast and extensible equality saturation

An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to ...
Improving Bit-Blasting for Nonlinear Integer Constraints
ISSTA 2023: Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis

Nonlinear integer constraints are common and difficult in the verification and analysis of software/hardware. SMT(QF_NIA) generalizes such constraints, which is a boolean combination of nonlinear integer arithmetic constraints. A classical method to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '98: Proceedings of the 35th annual Design Automation Conference

May 1998

820 pages

ISBN:0897919645

DOI:10.1145/277044

Chairmen:
Basant R. Chawla
Lucent Technologies, Warren, NJ
,
Randal E. Bryant
Carnegie Mellon Univ., Pittsburgh, PA
,
Jan M. Rabaey
Univ. of California, Berkeley
,
Editor:
M. J. Irwin

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 May 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

DAC98

Sponsor:

EDAC
SIGDA
IEEE-CS

DAC98: The 35th ACM/IEEE-CAS/EDAC Design Automation Conference

June 15 - 19, 1998

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

57
Total Citations
View Citations
175
Total Downloads

Downloads (Last 12 months)75
Downloads (Last 6 weeks)15

Reflects downloads up to 18 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Fan HHe F(2024)Leveraging Datapath Propagation in IC3 for Hardware Model CheckingIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.336002243:7(2215-2228)Online publication date: Jul-2024
https://doi.org/10.1109/TCAD.2024.3360022
Faure-Gignoux ADelmas KGauffriau APagetti C(2024)Methodology for Formal Verification of Hardware Safety Strategies Using SMTIEEE Embedded Systems Letters10.1109/LES.2024.343985916:4(381-384)Online publication date: Dec-2024
https://doi.org/10.1109/LES.2024.3439859
Trabish DItzhaky SRinetzky NSpinellis DGousios GChechik MDi Penta M(2021)A bounded symbolic-size model for symbolic executionProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3468264.3468596(1190-1201)Online publication date: 20-Aug-2021
https://dl.acm.org/doi/10.1145/3468264.3468596
Velasquez AJha SEwetz RJha S(2021)Automated Synthesis of Quantum Circuits using Symbolic Abstractions and Decision Procedures2021 IEEE International Symposium on Circuits and Systems (ISCAS)10.1109/ISCAS51556.2021.9401587(1-5)Online publication date: May-2021
https://doi.org/10.1109/ISCAS51556.2021.9401587
Yao PShi QHuang HZhang CKhurshid SPăsăreanu C(2020)Fast bit-vector satisfiabilityProceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3395363.3397378(38-50)Online publication date: 18-Jul-2020
https://dl.acm.org/doi/10.1145/3395363.3397378
Vijay JSridhar R(2020)EBV: Encoded Binary Vector for Efficient Information Retrieval, Query Processing and Recommendation for Travel and Tourism DomainArabian Journal for Science and Engineering10.1007/s13369-020-04982-wOnline publication date: 7-Oct-2020
https://doi.org/10.1007/s13369-020-04982-w
Sultana NStewart RMichaelson G(2019)What we talk about when we talk about pcap expressionsProceedings of the 4th ACM International Workshop on Real World Domain Specific Languages10.1145/3300111.3300113(1-9)Online publication date: 17-Feb-2019
https://dl.acm.org/doi/10.1145/3300111.3300113
Chihani ZMarre BBobot FBardin S(2017)Sharpening Constraint Programming Approaches for Bit-Vector TheoryIntegration of AI and OR Techniques in Constraint Programming10.1007/978-3-319-59776-8_1(3-20)Online publication date: 31-May-2017
https://doi.org/10.1007/978-3-319-59776-8_1
Bauch PHavel VBarnat J(2016)Control Explicit--Data Symbolic Model CheckingACM Transactions on Software Engineering and Methodology10.1145/288839325:2(1-48)Online publication date: 6-Apr-2016
https://dl.acm.org/doi/10.1145/2888393
Kovásznai GFröhlich ABiere A(2016)Complexity of Fixed-Size Bit-Vector LogicsTheory of Computing Systems10.1007/s00224-015-9653-159:2(323-376)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s00224-015-9653-1
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

A fast bit-vector algorithm for approximate string matching based on dynamic programming

egg: Fast and extensible equality saturation

Improving Bit-Blasting for Nonlinear Integer Constraints