Diploma Thesis
Abstract
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
@MISC{Moe98,
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/}},
}