Fast dieselbe Seite auf Deutsch 

Bit-Vector Research Page
BRICS

This page contains actual information about developments and results concerning the theory of bit-vectors with a special focus to the construction of solver algorithms.

 
 General Information

Bit-vectors are - in the context of hardware verification - data structures, which represent elements of a mutisorted logic (i.e. a bit-vector can be of the type bvec[1], bvec[2],...). The width 0 is illegal.The bits are counted from left to right, starting with 0. In contrast to arrays, bit-vectors are considered finite objects, each position containing a value out of a binary alphabet.
Typical operations are

Additionally, the following operations are found frequently: The main focus of the research in Ulm is to construct efficient solvers for a rich theory of bit-vector equations.
As it turnes out, it is a crucial point whether to allow variable width (e.g. vie introducing a dependend type bvec[n], where n is a integer variable itself) or variable extraction (terms x[i:j] where i and j are integer variables). If one of these operations is permitted, the theory is no longer convex in the sense that a solution is always a conjunction of equations.

 
 Group members

 
 Complexity Results

(dvi files)

 
 Canonizer and Solver

Those should be build according to the requirements from the theory of congruence closure (Nelson-Oppen), explicitly formalised in the CADE-paper 1996 of Patt Lincoln, David Cyrluk und Natarjan Shankar).
A solver for simple bit-vector terms (fix extraction, known length, no boolean connectors) was given in the technical report of Harald Ruess/Oliver Möller (both Ulm) and David Cyrluk (SRI), called "An Efficient Decision Procedure for a Theory of Fixed-Sized Bit-vectors with concatenation and extraction":

The next step was the introduction of boolean operators (David Cyrluk/Oliver Möller, SRI, October 96), using ordered binary decision diagrams (for a demonstration see OBDDs ).
The algorithm (in Common Lisp) was implemented and a paper titled "An Efficient Decision Procedure for the theory of Fixed-Sized Bit-Vectors" is published in the CAV97:
And a recent result, adressing non-fixed size is found here:

You might also get a short overview on the topic by looking through the prepared

 
 Recent Work

In connection with the work on the diploma thesis "Solving Bit-Vector Equations - A Decision Procedure for Hardware Verification" a number of decision procedures were implemented in Allegro Common Lisp and are available here:

Solver for Bit-Vector Theories [in ACL]
Solver: WS1S with MONA Reduced Chopper Fixed Solver Split-Chop
Allows fixed width
Boolean op's, Arithmetic
fixed width
just concatenation and extraction
fixed width
Boolean op's, Arithmetic
[includes heuristics]
variable width
concatenation and (variable) extraction
Size 14.6 KB 18.4 KB 22.1 KB 30.1 KB

Files
Contained

check_via_mona.cl
bvec_arith.cl
bvec_structure.cl
reduced_chopper.cl
bvec_arith.cl
bvec_structure.cl
bvec_fixed_solver.cl
bvec_slicing.cl
bvec_bdd_solve.cl
bvec_arith.cl
bvec_structure.cl
split_chop.cl
fm_elimination.cl
bvec_arith.cl
bvec_slicing.cl
bvec_structure.cl
gzipped tar archives, uncompress via gtar -xvzf ; to get all in one archive (73,4 KB), click here

The thesis itself can be obtained at Diploma Thesis. It contains a description of the solvers as well as some new complexity results. E.g. it is shown that no solver can exist for the theory of bit-vectors, if variable width, variable extraction and boolean operations are allowed.

If you have any comments, your feedback is apprechiated: webmaster@verify-it.de


Oliver Möller Last modified: Tue Aug 24 12:51:15 1999