bounce

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |

Bounce ist ein Bounded Model Checking Tool, welches die Nicht-Realisierbarkeit einer Invariante in einem unvollständigen Schaltkreis beweisen kann. Zur Modellierung des unbekannten Verhaltens der Blackboxes unterstützt bounce zum einen die 01X-Modellierung sowie mehrere QBF-Modellierungsverfahren, wobei als back-end Solver MiraXT für SAT Formeln und QuBE, AIGsolve und QMiraXT für QBF Formeln verwendet werden. Zusätzlich kann die 01X-Härte eines unvollständigen Systems durch die Berechnung von Craig Interpolanten in MiraXT gezeigt werden, was bedeutet, dass die 01X-Modellierung allein zu ungenau ist, um die Nicht-Realisierbarkeit zu beweisen. In einem weiteren Schritt kann bounce mittels auf den berechneten Craig Interpolanten und Unsatisfiable-Cores basierenden Heuristiken diejenigen Blackbox Ausgänge identifizieren, die mit QBF modelliert werden müssen. Bounce liest Gatter-Netzlisten im BBBLIF Format (BLIF Format erweitert um Blackbox Beschreibungen).

Bounce wurde mit VHDL Designs von http://www.opencores.org/ getestet. Zuerst werden Blackboxes und evtl. Fehler direkt in den VHDL Code eingefügt, welcher darauf mit Synopsys Design Compiler kompiliert und mit einer minimalen Gatterbibliothek (ein- und zwei-Input Gatter sowie Flipflops) zu Verilog synthetisiert wird. Die Verilog Designs können dann direkt in das BBBLIF Format übersetzt werden. Folgenden Benchmarks wurden verwendet:

FPU: Dieses Design ist eine IEEE-754 konforme Floating-Point-Unit, die die Grundrechenarten (+,-,*,/) sowie mehrere Rundungsmodi und Exceptions unterstützt. Die Instanzen unterscheiden sich in ihrer Initialisierung und in den Fehlern, die direkt in die Netzliste durch das Verändern von zufälligen Gattern eingefügt werden. Durchschnittlich bestehen die Instanzen aus ca. 21.000 Gattern und 2.700 Flipflops. Es wird die korrekte Berechnung des Vorzeichenbits bei der Addition und Subtraktion falsifiziert, wobei der Multiplizierer und Dividierer durch Blackboxes modelliert werden.

Plasma-MIPS: Das Plasma-MIPS Design ist ein einfacher 32-Bit Mikroprozessor, der alle MIPS Version I user mode Befehle unterstützt, wobei die Instanzen in der größe des Bootloaders variieren. Diese bestehen aus ca. 17.000 Gattern und 2.500 Flipflops (Multiplizierer und Shifter werden als Blackboxes modelliert). Es wird verifiziert, dass ein bestimmter Zustand des Bootloaders erreicht werden kann.

UART: Der UART Benchmark besteht aus zwei UART Einheiten (universal asynchronous receiver transmitter), die mit - je nach Instanz - unterschiedlichen Bitraten operieren. Es wird gezeigt, dass alle 8-Bit Eingangsdaten korrekt gesendet und empfangen werden können, auch wenn der UART Controller als Blackbox modelliert ist. Die Instanzen bestehen aus ca. 150 Flipflops und 1.300 Gattern.

QALU: Das QALU Design ist eine VLIW ALU, die mehrere logische Operationen in vier arithmetischen Einheiten, welche in ihrere Bitbreite variieren, unterstützt. Einige dieser Einheiten werden als Blackbox modelliert, und die Korrektheit der XOR Operation wird widerlegt. Dieser Benchmark ist eine Modifikation des VLIW ALU Designs aus den AVACS Fallstuiden.