Efficient formal verification of complex designs

Diese Dissertation befasst sich mit der Herausforderung einer effizienten formalen Hardware-Verifikation. Selbst in der Ära nach dem Mooreschen Gesetz, in der sich die Skalierung der Transistordichte verlangsamt hat, nimmt die architektonische Komplexität weiter zu. Die Sicherstellung der Korrektheit zunehmend großer und komplexer Designs, wie beispielsweise Prozessoren, ist nicht nur eine Herausforderung, sondern stellt auch einen Flaschenhals im Entwicklungsfluss der Electronic Design Automation (EDA) dar. Da es sich um einen zeitintensiven Schritt handelt, ist eine effiziente Gestaltung der formalen Verifikation unerlässlich. Die Arbeit konzentriert sich auf die formale Verifikation von RISC-V-Prozessordesigns sowie auf die grundlegenden Bausteine neuromorpher Prozessoren, wie Multiply-Accumulate- (MAC) und Dot-Product-Einheiten (DP).

Für die Verifikation von Single- und Multi-Cycle-RISC-V-Designs wurde ein Prozess entwickelt, der die effiziente funktionale Verifikation der RV32I-Basisinstruktionen mithilfe von binären Entscheidungsdiagrammen (BDDs) ermöglicht. Die Effizienz dieses Verifikationsflusses ergibt sich aus der BDD-Datenstruktur selbst sowie aus der Erzeugung der BDDs mittels des ITE-Operators (If-Then-Else), was eine polynomial begrenzte BDD-Erzeugung und somit auch eine begrenzte Verifikation erlaubt. Über den RV32I-Befehlssatz hinaus wurden auch Multiplikationsinstruktionen der RISC-V-M-Erweiterung unter Verwendung eines erweiterten Verifikationsprozesses verifiziert, der symbolische Computeralgebra (SCA) integriert.

Der zweite Teil dieser Arbeit besteht aus mehreren Beiträgen. Erstens zeigte eine erste Machbarkeitsstudie für MAC- und DP-Einheiten unter Verwendung von SCA vielversprechende Ergebnisse und eine hohe Skalierbarkeit für einfache Designs. Zweitens wurde eine Skalierbarkeitsanalyse unter Design-Constraints wie Flächen- und Delay-Optimierung durchgeführt. Um die Wahrscheinlichkeit der Verifizierbarkeit vorherzusagen, wurden Skalierbarkeitsindikatoren entwickelt, die angeben, ob ein Design mit geringer Bitbreite auch bei der Skalierung auf größere Bitbreiten verifizierbar bleibt. Über strukturell einfache Designs hinaus wurden auch optimierte Verhaltensdesigns berücksichtigt, für die neue Techniken wie die transformationsgestützte Verifikation entwickelt und untersucht wurden. Diese zeigten vielversprechende Ergebnisse hinsichtlich der Wirksamkeit solcher Transformationen zur Abschwächung der intermediären Term-Explosion in der SCA-basierten Verifikation. Schließlich wird ein erster Beweis für eine Obergrenze präsentiert, der aus Regeln für And-Inverter-Graphen (AIG) abgeleitet wurde. Eine entsprechende Fallstudie für Carry-Ripple-Addierer demonstriert den Einfluss der Traversierungsreihenfolge und die Effektivität der Graph-Splitting-Methode, um die primären Ausgänge separat und isoliert zu verifizieren.