Almost the same page in English

 

Allgemeine Informationen

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.

• 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.

 

Mitarbeiter

• Dr. Harald Rueß
• Oliver Möller

 

Komplexitätstheoretische Ergebnisse

(als englischsprachige dvi-Files abgelegt)

• Ein NP-vollständiges Problem: BVEVE-Solvability
• Ein NP-hartes Problem: BV[n]-Solvability
• Die Unvollständigkeit ist gar nicht weit - exists-BV[n]-Solvability

 

Kanonisierer und Solver

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:

• Ulmer Informatik-Berichte 96-9
  

• CAV'97