Zum Hauptinhalt springen

Formale Verifikation von arithmetischen Schaltungen

Das heutige Thema im Fokus gibt einen Einblick in die Dissertation „Formal Verification of Multiplier Circuits using Computer Algebra“ unserer diesjährigen Dissertationspreisträgerin Daniela Kaufmann (Dissertation: danielakaufmann.at).

Sie lesen dieses GI-Radar gerade an einem Bildschirm, haben vielleicht noch ein Smartphone neben sich liegen und tragen möglicherweise auch noch eine Smartwatch am Handgelenk. Computer werden heutzutage nicht nur im persönlichen Umfeld eingesetzt, sondern etwa auch im Finanzwesen, zur Verkehrsflussregelung oder in Intensivstationen. In diesen sicherheitsrelevanten Bereichen ist die korrekte Funktion eines Computers unabdingbar.

Digitale Schaltungen sind ein wesentlicher Bestandteil von Computern und digitalen Systemen. Diese Schaltungen implementieren logische Funktionen und können zahlreiche digitale Komponenten und arithmetische Operationen modellieren. Die Hauptkomponenten digitaler Schaltungen sind Logikgatter, welche einfache Boolesche Funktionen repräsentieren. Beispiele für diese Gatter sind Negation (NOT), Konjunktion (UND) und Disjunktion (ODER). Diese logischen Gatter können kombiniert werden, um komplexere Funktionen darzustellen. Eine Unterkategorie von digitalen Schaltungen sind Schaltnetze. Schaltnetze werden in Computern eingesetzt, um Boolesche Algebra zu implementieren. Zum Beispiel ist die arithmetisch-logische Einheit (ALU) in einem Prozessor, die zur Berechnung von mathematischen Operationen eingesetzt wird, aus Schaltnetzen konstruiert. Arithmetische Schaltungen sind spezielle Schaltnetze, die Rechenoperationen wie zum Beispiel Multiplikation durchführen.

Aufgrund des weitreichenden, mitunter sicherheitskritischen Einsatzes von digitalen Schaltungen ist es äußerst wichtig, ihre Korrektheit sicherzustellen. Fehler in den Schaltungen können fatale Folgen in der Anwendung haben. Ein berühmtes Beispiel für eine fehlerhafte Schaltung ist der FDIV-Bug in frühen Intel Pentium Prozessoren (heise). Die Gleitkommaeinheit (FPU) dieser Prozessoren enthält einen Hardwarefehler, der bei Division von bestimmten Zahlen zu falschen Ergebnissen führt. Im schlimmsten Fall ist bereits die vierte Nachkommastelle falsch. Der Fehler wurde erst 1994, rund eineinhalb Jahre nach Markteinführung des Prozessors bekannt und kostete Intel damals ca. 500 Millionen US-Dollar (uni-jena.de). Eine gleichartige Panne würde heutzutage wohl ernsthafte finanzielle Schwierigkeiten, auch für große Prozessorhersteller, bedeuten. Daher wollen diese Firmen die Korrektheit ihrer Hardware zu hundert Prozent garantieren können.

Eine Möglichkeit die Korrektheit sicherzustellen wäre es, alle möglichen Zustände der Eingangssignale einer Schaltung zu überprüfen. Dies skaliert jedoch nicht, denn jedes Eingangssignal kann die binären Werte 0 und 1 annehmen. Das heißt, mit jedem zusätzlichen Eingangssignal verdoppelt sich die Menge der Testfälle. Bei Schaltungen mit 8 Eingängen sind dies 256 Testfälle, bei 9 Eingängen sind es bereits 512 Testfälle. Bei Schaltungen mit mehr als 300 Eingängen übersteigt die Anzahl der Testfälle bereits die Anzahl der Atome im beobachtbaren Universum (youtube.com). Man kann sich also leicht vor Augen führen, dass das Testen von großen Schaltungen nicht zielführend ist, um deren Korrektheit zu bestimmen.

Mittels formaler Verifikation lässt sich die Korrektheit von Software oder Hardware in Bezug auf eine zuvor definierte Spezifikation formal beweisen. Dazu wird das gegebene System in ein mathematisches Modell übersetzt und automatisierte Beweistechniken werden eingesetzt, um die gewünschten Korrektheitsbeweise zu erzielen. Die verschiedenen Verifikationstechniken unterscheiden sich durch die zugrundeliegenden mathematischen Modellierungen des Systems.

Mehr als 25 Jahre nach Bekanntwerden des FDIV-Bugs ist die automatisierte Verifikation von Schaltungen jedoch noch immer nicht vollautomatisiert lösbar. Besonders Integer-Multiplizierer, das sind arithmetische Schaltungen, die Multiplikationen von ganzen Zahlen ausführen, stellen aufgrund ihres internen Aufbaus der Logikgatter eine Herausforderung für bestehende Verifikationsmethoden dar. In der Praxis bedeutet dies, dass industrielle Entwickler von arithmetischen Schaltungen momentan entweder aufwändige manuelle Verifikation mittels Theorembeweisern betreiben, oder sich komplett auf Simulationen verlassen. Immer bessere Optimierungen in der Entwicklung erhöhen einerseits die Effizienz einer Schaltung, steigern andererseits aber deren Komplexität. Daher gelten Simulationen in der Praxis nicht mehr als vertrauenswürdig. Das Fehlen von vollautomatisierten Verifikationsmethoden für arithmetische Schaltungen ist aktuell immer noch ein großer Makel.

Seit dem Bekanntwerden des FDIV-Bugs werden formale Verifikationstechniken entwickelt, welche die Korrektheit von arithmetischen Schaltungen und insbesondere von Multiplizierern beweisen sollen. Eine gängige Verifikationsmethode ist, das Verifikationsproblem als ein Erfüllbarkeitsproblem der Aussagenlogik (SAT) zu kodieren. SAT wird unter anderem als „key technology for the 21st century“ (Edmund Clark, 2007 ACM Turing Award Recipient) bzw. als „killer app“ (Donald Knuth, 1974 ACM Turing Award Recipient) gesehen (iospress.com). Bei dieser Methode wird die Schaltung zu einer Formel in konjunktiver Normalform übersetzt und ein SAT-Solver eingesetzt, um die Erfüllbarkeit dieser Formel zu überprüfen. Im Jahr 2016 wurde eine größere Menge von solchen Kodierungen für arithmetische Schaltungen als Benchmarks zur jährlichen SAT-Competition eingereicht (satcompetition.org). Bei diesem Wettbewerb werden die aktuell besten SAT-Solver anhand einer Menge von Benchmarks ermittelt. Die Ergebnisse dieser Evaluierung zeigen allerdings, dass Kodierungen von Multiplizierern zu exponentiell großen Beweisen führen; dies deutet auf eine exponentielle Laufzeit von SAT-Solvern hin.

Seit rund 5 Jahren werden Verifikationstechniken basierend auf Computeralgebra als ein vielversprechender Zugang zur automatisierten Verifikation von arithmetischen Schaltungen und insbesondere Multiplizierern gesehen. Computeralgebra beschäftigt sich mit der Entwicklung von Algorithmen für exakte Lösungen für komplexe mathematische Probleme. In dieser Methode werden alle Logikgatter des Multiplizierers sowie die Spezifikation als ein Polynom kodiert. Mittels algebraischer Reduktion basierend auf multivariater Polynomdivision kann nun das Problem, ob eine gegebene Schaltung einen korrekten Multiplizierer implementiert, gelöst werden, indem die Normalform des Spezifikationspolynoms bezüglich der Gatterpolynome berechnet wird. Der Multiplizierer ist fehlerfrei genau dann, wenn diese Normalform null ist.

Das klingt auf den ersten Blick offensichtlich, doch wie so oft, ist es in der Praxis dann doch nicht so leicht, wie es klingt. Experimente zeigen, dass bereits für einfache 8-Bit-Multiplizierer mit 16 Eingängen die Normalform der Spezifikation nicht mehr in gängigen Computeralgebra-Systemen ermittelt werden kann. Der Grund dafür ist, dass die Zwischenresultate der einzelnen Polynomdivisionen exponentiell anwachsen, bevor sie zu null reduzieren. Daher sind in der Praxis dedizierte Vorbearbeitungsschritte notwendig, um die mathematische Modellierung des Multiplizierers zu vereinfachen. Mit diesen Techniken ist es heutzutage möglich, 2048-Bit-Multiplizierer mit 4096 Eingangssignalen innerhalb einer Stunde erfolgreich in eigens entwickelten Verifikationstools zu verifizieren.

An dieser Stelle kann man sich die Frage stellen: Wer verifiziert eigentlich den Verifizierer? Denn auch in der Verifikation können Fehler passieren und zu falschen Ergebnissen führen. Eine Möglichkeit ist es, das Verifikationstool mit Hilfe eines Theorembeweisers zu verifizieren. Dies gilt aber aufgrund der Komplexität der Software als nicht praktikabel. Eine einfachere Methode ist es daher, ein simples Beweiszertifikat zu erstellen, welches es ermöglicht, die Verifikationsschritte nachzuvollziehen und unabhängig zu überprüfen. Man kann sich das ähnlich zu einer Rechenprobe wie bei Division von Zahlen vorstellen. Für SAT ist dieses Prozedere bereits gang und gäbe und wird seit 2013 auch in der jährlichen SAT-Competition vorgeschrieben. Für algebraische Beweistechniken werden seit rund 3 Jahren praktische Beweisformate entwickelt, welche es erlauben, während der Verifikation ein simples Beweiszertifikat zu generieren. Diese Zertifikate können dann mit einem eigenständigen Beweis-Checker auf Korrektheit überprüft werden (danielakaufmann.at).

Und wer beweist nun den Beweis-Checker? Es kann immer noch der Fall eintreten, dass während der Verifikation ein Fehler gemacht worden ist, der auch im Beweiszertifikat enthalten ist, aber vom Beweis-Checker nicht erkannt wird. An dieser Stelle kann man sich zu Nutze machen, dass Beweis-Checker üblicherweise sehr einfache Tools sind. Für Verifikation mittels Computeralgebra sind im Beweis-Checker nur die Operationen Polynomaddition und -multiplikation notwendig. Diese Operationen lassen sich in einem Theorembeweiser, wie etwa Isabelle/HOL, zertifiziert implementieren (tum.de). Vereinfacht gesagt basieren Theorembeweiser auf einem minimalen Kernel, der so simpel ist, dass man ihm vertraut. Jegliche zusätzliche benötigte Operation muss im Theorembeweiser formal bewiesen werden, um die Korrektheit garantieren zu können. Können wir also die Korrektheit von einem Multiplizierer mit einem Verifikationstool beweisen, und das zugehörige Beweiszertifikat wird von einem zertifizierten Beweis-Checker validiert, können wir uns der Korrektheit der Schaltung sicher sein.

Wir danken Frau Kaufmann, die diesen in ihr Forschungsgebiet einführenden Text geschrieben hat.

© Ryan - Unsplash