A decision procedure for bit-vector arithmetic

Clark W. Barrett, David L. Dill, Jeremy R. Levitt

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Bit-vector 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 such a theory is NP-hard, our implementation is efficient for many practical examples. We believe this to be the first such implementation which is efficient, automatic, and complete.

Original languageEnglish (US)
Title of host publicationProceedings 1998 - Design and Automation Conference, DAC 1998
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages522-527
Number of pages6
ISBN (Print)078034409X
DOIs
StatePublished - 1998
Event35th Design and Automation Conference, DAC 1998 - San Francisco, United States
Duration: Jun 15 1998Jun 19 1998

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X

Conference

Conference35th Design and Automation Conference, DAC 1998
CountryUnited States
CitySan Francisco
Period6/15/986/19/98

ASJC Scopus subject areas

  • Computer Science Applications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering
  • Modeling and Simulation
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'A decision procedure for bit-vector arithmetic'. Together they form a unique fingerprint.

  • Cite this

    Barrett, C. W., Dill, D. L., & Levitt, J. R. (1998). A decision procedure for bit-vector arithmetic. In Proceedings 1998 - Design and Automation Conference, DAC 1998 (pp. 522-527). [724527] (Proceedings - Design Automation Conference). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/277044.277186