Solving Bit-Vector Equations - A Decision Procedure for Hardware Verification 

M. Oliver Möller

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.