TY - GEN
T1 - A decision procedure for bit-vector arithmetic
AU - Barrett, Clark W.
AU - Dill, David L.
AU - Levitt, Jeremy R.
N1 - Funding Information:
We would like to thank Yirng-An Chen for his help in understanding and using *BMDs. We would like to thank other members of the TORCH verification effort for their work in rpecifying and translating examples for this paper: Jeffrey ju, Jens Skakkebaek, and especially Laurent Arditi who also xovided insight and analysis for comparison with *BMDs. .llso, we would like to thank the group at SRI International ior valuable discussions, especially David Cyrluk whose work on bit-vectors provided a valuable starting point. This work ivas sponsored by DARPA contract number DABT63-96-C- 0097 and by a National Defense Science and Engineering Graduate Fellowship. The content of this paper does not necessarily reflect the position of the policy of the government and no official endorsement should be inferred.
Publisher Copyright:
© 1998 ACM.
PY - 1998
Y1 - 1998
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0031618668&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0031618668&partnerID=8YFLogxK
U2 - 10.1145/277044.277186
DO - 10.1145/277044.277186
M3 - Conference contribution
AN - SCOPUS:0031618668
SN - 078034409X
T3 - Proceedings - Design Automation Conference
SP - 522
EP - 527
BT - Proceedings 1998 - Design and Automation Conference, DAC 1998
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 35th Design and Automation Conference, DAC 1998
Y2 - 15 June 1998 through 19 June 1998
ER -