Universität Ulm, Fakultät für Informatik, Abt. KI - Back to the Bit-Vector Research Page

Solving Bit-Vector Equations
A Decision Procedure for Hardware Verification

M. Oliver Möller

Diploma Thesis


This thesis investigates the problem of solving bit-vector equations both from a theoretical and practical side. Complexity and decidability of bit-vector theories including concatenation, extraction, bit-wise boolean operations and arithmetic are observed. Boolean operations on are introduced by means of ordered binary decision diagrams, which also provide a conceptually clean way to encode arithmetic. Generalizations that allow the width of bit-vector variables to be unknown are discussed as well. Surprisingly, extensions that maintain the fixed size lead to theories that are releated in the way, that for all of them the word problem is NP-complete. As expected, far reaching extention of the bit-vector theory leads neccessarily to the incompleteness of any solver algorithm. A proof is obtained by reduction of the halting problem. Furthermore, a more accurate characterization of the expressiveness of solving is developed. In general, solving algorithms can be utilized to decide quantified equations, which is made explicit in the Quantification Lemma.
On the practical side, several approaches for solving bit-vector theories are explored in this thesis. The task of solving fixed-sized equations is performed by means of a translation to weak second order monadic logic, an equational transformation system and an operationalized and efficient version of the latter, supported by heuristics. These approaches are corroborated by implementations and run-time experiments. Finally, a general concept for solving bit-vector equations with variable width is given. The algorithms presented in this thesis have all been implemented and can be obtained at the Bit-Vector Research Page in Ulm.

Available as Postscript (1.38 MB) or compressed Postscript (484 KB).

BibTeX Entry

AUTHOR = {M. Oliver M{\"o}ller},
TITLE  = {{S}olving {B}it-{V}ector {E}quations - {A} {D}ecision {P}rocedure for {H}ardware {V}erification},
YEAR = {1998},
SCHOOL = {University of Ulm, Germany},
NOTE = {Diploma Thesis, available at
        {\tt http://www.informatik.uni-ulm.de/ki/Bitvector/}},

Oliver Möller - March 20, 1998 - Mail to Webmaster