DocumentCode
2099621
Title
A decision procedure for bit-vector arithmetic
Author
Barrett, Clark W. ; Dill, David L. ; Levitt, Jeremy R.
Author_Institution
Comput. Syst. Lab., Stanford Univ., CA, USA
fYear
1998
fDate
19-19 June 1998
Firstpage
522
Lastpage
527
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.
Keywords
digital arithmetic; formal verification; NP-hard; bit-vector arithmetic; decision procedure; hardware verification; Arithmetic; Boolean functions; Data structures; Design automation; Explosions; Hardware; Laboratories; Microprocessors; Permission; Static VAr compensators;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 1998. Proceedings
Conference_Location
San Francisco, CA, USA
Print_ISBN
0-89791-964-5
Type
conf
Filename
724527
Link To Document