Core Concepts
SEPE-SQED nutzt Programmsynthese, um Instruktionssequenzen zu finden, die semantisch äquivalent zu Originalinstruktionen sind. Dadurch können sowohl Einzelinstruktions- als auch Mehrfachinstruktionsfehler im Prozessordesign effizient erkannt werden.
Abstract
Der Artikel stellt einen neuen Ansatz zur formalen Verifikation von Prozessoren vor, der als symbolische schnelle Fehlererkennung durch semantisch äquivalente Programmausführung (SEPE-SQED) bezeichnet wird.
SEPE-SQED erweitert den bestehenden SQED-Ansatz, indem er Programmsynthese-Techniken nutzt, um Instruktionssequenzen zu finden, die semantisch äquivalent zu den Originalinstruktionen sind. Dadurch können sowohl Einzelinstruktions- als auch Mehrfachinstruktionsfehler im Prozessordesign effizient erkannt werden.
Der Kern des Ansatzes ist, dass SEPE-SQED die Korrektheit einer Implementierung überprüft, indem es die Ausführung der Originalinstruktion mit der Ausführung ihres semantisch äquivalenten Programms vergleicht. Einzelinstruktionsfehler, die sich unterschiedlich auf die Originalinstruktion und ihr semantisch äquivalentes Programm auswirken, führen so zu einem Konsistenzbruch, der erkannt werden kann.
Um den mit der Programmsynthese verbundenen großen Suchraum zu bewältigen, stellt der Artikel den HPF-CEGIS-Algorithmus vor, der im Vergleich zu früheren CEGIS-Ansätzen die gewünschten Programme mit einer durchschnittlichen Zeitersparnis von 50% synthetisiert.
Die experimentellen Ergebnisse zeigen, dass SEPE-SQED in der Lage ist, sowohl Einzelinstruktions- als auch Mehrfachinstruktionsfehler in einem realen leistungsfähigen Open-Source-Prozessor zu erkennen. In bestimmten Szenarien kann SEPE-SQED sogar kürzere Fehlerspuren als SQED generieren.
Stats
SEPE-SQED kann Einzelinstruktionsfehler in durchschnittlich 1436,46 Sekunden erkennen.
SEPE-SQED kann Mehrfachinstruktionsfehler in durchschnittlich 1000 Sekunden erkennen, was teilweise schneller ist als SQED.
Der HPF-CEGIS-Algorithmus reduziert die Synthesezeit für semantisch äquivalente Instruktionssequenzen im Durchschnitt um 50% im Vergleich zu früheren Methoden.
Quotes
"SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence)."
"Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios."