VAPA Verifikation moderner Prozessor-Architekturen

Ziele

In diesem von der German-Israeli-Foundation (G.I.F.) geförderten Projekt geht es um die Entwicklung einer auf Verfeinerungstechniken basierenden Methodik zur Verifikation moderner Prozessor-Architekturen.

Moderne Prozessor-Architekturen wie beispielsweise der Power-PC oder die DEC-Alpha CPU verwenden aggressive Implementierungstechniken, um einen möglichst großen Instruktionsdurchsatz zu erreichen. Die durch Techniken wie Out-Of-Order-Execution, Mehrfachinitialisierung von Instruktionen, dynamische Sprungvorhersage, spekulative Instruktionsausführung und schwache Speicherkonsistenzmodelle induzierte Komplexität machen Implementierungen dieser Prozessor-Architekturen extrem fehleranfällig und somit die Anwendung formaler Verifikationsmethoden zur Validierung von Korrektheitseigenschaften nötig.

Ziel des Projekts ist die Entwicklung einer auf Verfeinerungs-(Refinement-)Techniken basierenden Methodik, mit der die Verifikation solcher modernenProzessor-Architekturen ermöglicht wird. Bei diesem Ansatz gilt eine CPU-Implementierung dann als korrekt, wenn sie kompatibel zu einer Referenz-Architektur ist, bei der Instruktionen in streng sequentieller Reihenfolge gemäß der Programmordnung abgearbeitet werden.

Personen

Laufzeit

Start: 01.01.1999
Ende: 31.12.2001