An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors
(David Cyrluk, M. Oliver Möller, and Harald Rueß)
Abstract
In this paper we describe a decision procedure for the core theory of
fixed-sized bit-vectors with extraction and composition than can readily be
integrated into Shostak's procedure for deciding combinations of
theories. Inputs to the solver are unquantified bit-vector equations t = u and
the algorithm returns true if t = u is valid in the bit-vector theory, false
if t = u is unsatisfiable, and a system of solved equations otherwise. The
time complexity of the solver is O(|t|*log(n) + n^2), where t is the length of
the bit-vector term t and n denotes the number of bits on either side of the
equation. Then, the solver for the core bit-vector theory is extended to
handle other bit-vector operations like bitwise logical operations, shifting,
and arithmetic interpretations of bit-vectors. We develop a BDD-like
data-structure called bit-vector BDDs to represent bit-vectors, various
operations on bit-vectors, and a solver on bit-vector BDDs. The overall
procedure has been integrated with the decision procedures of the PVS
prover. The implementation has been tested with typical lemmas from the domain
of microprocessor verification. The implementation has also been applied to
proofs found in the verification of a commercial microprocessor. By using our
decision procedure for bit-vectors we have simplified a number of proofs by
eliminating manual proof steps that were previously necessary for reasoning
about bit-vectors.