An Efficient Decision Procedure for a Theory of Fixed-Sized Bitvectors with Composition and Extraction

D. Cyrluk, O. Möller, H. Rueß

Abstract

The theory of fixed-sized bitvectors with composition and extraction has been shown to be useful in the realm of hardware verification, and in this paper we develop an efficient algorithm for deciding this theory. A proper input is an unquantified bitvector equation, say t = u, and our algorithm returns true if t = u is valid in the bitvector theory, false if t = u is unsatisfiable, and a system of solved equations otherwise. The time complexity of this solver is O(|t| log(n) + n^2), where |t| is the length of the bitvector term t and n denotes the number of bits on either side of the equation. Moreover, the resulting procedure can readily be integrated into Shostak's procedure for deciding combinations of theories.

Available as Postscript (280 KB) or compressed Postscript (107 KB).

BibTeX Entry

@TechReport{CMR96,
  author    = "D. Cyrluk and O. M{\"o}ller and H. Rue{\ss}",
  title     = "An {E}fficient {D}ecision {P}rocedure
               for a {T}heory of {F}ixed-{S}ized {B}itvectors
               with Composition and Extraction",
  year      = "1996",
  number    = "96-8",
  institute = "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  type      = "Ulmer Informatik-Berichte"
}