Die Bit-Vector Research Page auf Deutsch
Diese Seite enthält aktuelle Informationen über die neueren Entwicklungen und Erkenntnisse in der Theorie der Bitvektoren, insbesondere hinsichtlich Entscheidungsprozeduren.
Bitvektoren sind - im Kontext der Hardwareverifikation - Datenstrukturen, die Elemente einer mehrsortigen Logik repräsentieren, d.h. es gibt die Typen bvec[1], bvec[2], usw. Die Breite '0' ist nicht erlaubt. Die Bits werden von links nach rechts durchnummeriert, beginnend mit Position 0. Bitvektoren werden (im Gegensatz zu Arrays) als endlich
angesehen und enthalten (normalerweise) and jeder Position nur '0' oder '1' (bzw. 'false' oder 'true').
Typische Operationen sind
- Extraktion :: <bvec> [<nat> , <nat>]
z.B. x [0:6] meint die 7 am weitesten links stehenden Bits von x (x: bvec[n] mit n >= 7)
- Konkatenation :: <bvec> o <bvec>
d.h. das assoziative Aneinanderhängen von Bitvektoren (z.B.: x o y o z)
- Fill :: Fill[<nat>](<Bit>)
Also ein Bitvektor der Länge n, der lauter identische Bits enthält.
Das Bit kann dabei eine Konstante (d.h. 0 oder 1) oder eine Variable sein.
Außerdem findet man häufig folgende Operationen:
- Logische (Bool'sche) Operatoren :: NOT <bvec>, <bvec> AND <bvec> , ...
Die Argumente müssen dann natürlich vom gleichen Typ sein (d.h. gleich lang)
- Arithmetische Operationen :: +, *
Üblicherweise ist damit Arithmetik modula 2^n gemeint. Das Bit an Position 0 (d.h. am weitesten links) ist dabei die am wenigsten gewichtete Stelle.
- Bitextract :: <bvec> ^ (<nat>)
Liefert erwartungsgemäß ein Bit
- bv2nat(<bvec>) und nat2bv[<nat>](<nat>)
Umrechnung von Bitvektoren in natürliche Zahlen (und umgekehrt);
Bei nat2bv wird normalerweise die Länge des Ergebnis-Vektores explizit angegeben.
Das Hauptaugenmerk der Forschung in Ulm liegt bei der Entwicklung von Solvern zum automatischen lösen von Bit-Vektor Gleichungen.
Wie sich zeigt, ist es eine kritische Entscheidung, ob Bit-Vektoren unbekannter Länge (d.h von einem abhängigen Datentyp bvec[n], wobei n selber eine Integervariable ist) oder variable Extraktionen (d.h. x[i:j], wenn i und j Integervariablen sind) zugelassen werden sollen. In beiden Fällen ist die Theorie der Bit-Vektoren nicht mehr konvex, d.h. die allgemeinste Lösung läßt sich nicht immer als Konjunktion von Gleichungen der Form x = ..., y = ... darstellen.
Komplexitätstheoretische Ergebnisse |
(als englischsprachige dvi-Files abgelegt)
Diese sollten den Ansprüchen der "congruence closure"-Theorie von Nelson-Oppen genügen (explizit fomuliert im CADE-Paper 1996 von Patt Lincoln, David Cyrluk und Natarjan Shankar).
Ein brute-force Ansatz zur Lösung einfacher Bitvektor-Terme (d.h. fixe
Extraktion, bekannte Länge, keine logischen Konnektoren) ist im
technischen Bericht "An Efficient Decision Procedure for a theory of
Fixed-Sized Bitvectors with Composition and Extraction" von
Harald Ruess/ Oliver Möller (beide Ulm) / David Cyrluk (SRI) gegeben:
Als nächster weiterführender Schritt wurden logische Konnektoren zugelassen (David Cyrluk/Oliver Möller, SRI, Oktober 96). Dazu wurden Binäre Entscheidungsbäume ( OBDDs ) eingesetzt.
Bisher existiert dazu der Algorithmus (in Common Lisp) und ein Artikel, der in der CAV97 vorgestellt wurde (Titel: "An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors")
Ein etwa jüngeres Ergebnis wurde im Herbst '98 veröffentlicht:
Einen knappen Überblick geben die dazu vorbereiteten Folien:
In Zusammenhang mit der Diplomarbeit "Solving Bit-Vector Equations - A Decision Procedure for Hardware Verification" entstanden eine Reihe von Implementierungen von Solvern in Allegro Common Lisp. Sie können hier für eigene Experimente oder Erweiterungen heruntergeladen werden:
Solver für Bit-Vektor Theorien [in ACL]
Solver: |
WS1S with MONA |
Reduced Chopper |
Fixed Solver |
Split-Chop |
Erlaubte Bit-Vektor Operationen |
fixe Breite
Bool'sche Verknüpfung,
Arithmetik
|
fixe Breite
jnu Konkatenation und Extraktion
|
fixe Breite
Bool'sche Operationen,
Arithmetik
[inklusive Heuristiken] |
variable Breite
Konkatenation und (variable) Extraktion |
Filegröße |
14.6 KB |
18.4 KB |
22.1 KB |
30.1 KB |
Enthaltene Dateien |
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
|
Alle Files sind GNU gzippte tar Archive, entpacken mit: gtar -xvzf
Um alle Lisp-Files auf einmal zu erhalten (73,4 KB), hier klicken. |
Die Diplomarbeit selber is hier zu erhalten. Sie ist auf Englisch verfaßt und enthält eine Beschreibung der Solver. Darüber hinaus sind ein paar neue komplexitätstheoretische Ergebnisse drin. Das wichtigste ist vermutlich der Beweis, daß es für die Bit-Vektor Theorie mit variabler Breite, variabler Extraktion und Bool'schen Operationen keinen vollständigen Solver geben kann.
Für Feedback oder Anregungen bin ich jederzeit dankbar. webmaster@verify-it.de
Oliver Möller -
Last modified: Tue Aug 24 12:57:09 1999