Invariantengenerierung für die Verifikation von System-on-Chip-Protokollimplementierungen

*Deutsch:* Da die formale Eigenschaftsprüfung die vollständige Korrektheit eines Hardware-Designs garantiert, ist sie in den vergangenen Jahren erfolgreich in der Industrie eingeführt worden. Insbesondere Beweistechniken, welche auf einem beschränkten Modell (bounded model) die unbeschränkte Gültigkeit einer Eigenschaft (unbounded proof ) zeigen, wurden erfolgreich von der Industrie angenommen. Zu diesen Verfahren zählt unter anderem Interval Property Checking (IPC). Diese Verifikationstechnik wurde in den 90er Jahren des vergangenen Jahrhunderts entwickelt und industriell verwendet. Es handelt sich dabei um eine SAT-basierte Verifikationstechnik, die auf einem beschränkten konkreten Modell des zu untersuchenden Designs arbeitet. Eigenschaften werden dabei über einem endlichen Intervall formuliert. Das Modell wird durch Abrollen des Designs über eine Anzahl von Takten erzeugt. Die Eigenschaft wird durch eine aussagenlogische Formel, basierend auf den Variablen des abgerollten Designs, ausgedrückt. Da der SAT-Solver einen beliebigen Zustand als Anfang für die Eigenschaft annimmt, wird die unbeschränkte Gültigkeit der Eigenschaft auf dem Design garantiert, wenn der Beweis der Eigenschaft gelingt. Dies ist der Hauptunterschied zum Bounded Model Checking, welches nur einen beschränkten Nachweis der Korrektheit ermöglicht. Der Nachteil von IPC ist, dass so genannte False Negatives entstehen können, da der Anfangszustand des Eigenschaftsnachweises auf Grund der Beweismethodik nicht zwangsläufig im Design erreichbar sein muss. Diesem Phänomen kann durch Hinzufügen von Erreichbarkeitsbedingungen in Form einer Invariante, welche die Anfangszustände auf die Menge der erreichbaren Zustände beschränkt, begegnet werden. Für gewöhnlich spiegeln diese Invarianten einfache Beziehungen zwischen den Zustandsvariablen wider, die von einem Verifikationsingenieur leicht manuell gefunden werden können. Diese manuelle Ermittlung stellt jedoch einen äußerst zeitaufwändigen und fehleranfälligen Prozess dar. Aus diesem Grund wurde in dieser Arbeit ein Verfahren zur automatischen Generierung von Erreichbarkeitsbedingungen weiterentwickelt, so dass Invarianten vollautomatisch generiert werden konnten, welche stark genug sind, um sämtlich False Negatives zu eliminieren.