Verifikation eingebetteter Systeme - Wintersemester 2013/14

Viele moderne Produkte basieren auf mikroelektronischen Komponenten. Oftmals ist das korrekte Funktionieren dieser Produkte lebenswichtig, etwa in Medizintechnik oder Autoelektronik. Daher werden hohe Anforderungen an die Qualität der darin eingesetzten mikroelektronischen Systeme gestellt. Die Anforderungen lassen sich in drei Gruppen unterteilen: (1) Das System muss korrekt entsprechend der Spezifikation entworfen sein. (2) Das gemäß Entwurf physikalisch gefertigte System soll zum Zeitpunkt seiner Herstellung fehlerfrei funktionieren. (3) Darüber hinaus soll das System für einen gegebenen Zeitraum zuverlässig (d.h. ohne Ausfall) eingesetzt werden können.

Während Anforderung (2) durch Testmethoden und Anforderung (3) durch Methoden zur Erhöhung der Ausfallsicherheit behandelt werden, spielen für die Einhaltung von Anforderung (1) Verifikations- und Validierungsmethoden eine zentrale Rolle. Bei der heutzutage vorliegenden Komplexität der Systeme ist ein vollständiges Simulieren bei weitem nicht mehr möglich. Wird bei der Simulation des Entwurfs ein fehlerhaftes Verhalten festgestellt, so ist der Entwurf tatsächlich fehlerhaft. Wird jedoch kein Fehler gefunden, kann keine Aussage getroffen werden: Entweder ist der Entwurf tatsächlich korrekt oder er ist fehlerhaft, aber es wurde keine Eingabe simuliert, die zu fehlerhaftem Verhalten führt. Um systematisch Fehler zu finden und auch die Korrektheit eines Entwurfs zeigen zu können, wurden ausgefeilte Verfahren entwickelt, die heutzutage auch standardmäßig in der Industrie eingesetzt werden. Alle großen Hardwarefirmen wie Intel, AMD, Infineon setzen Verifikationsverfahren ein, um Fehler in den Chipentwürfen zu finden.

Der Schwerpunkt der Vorlesung liegt auf Verifikationsmethoden für digitale Komponenten. Dabei interessiert sowohl der formale Nachweis von Systemeigenschaften als auch die Übereinstimmung des Entwurfs im Vergleich zu einer gegebenen Spezifikation. Es werden zunächst verschiedene existierende Basistechniken zur formalen Verifikation vorgestellt, wie z. B. Binary Decision Diagrams und SAT-Solver. Darauf aufsetzend werden Ansätze zum Äquivalenzvergleich sowie zur Eigenschaftsprüfung beschrieben.