Vorlesung

Hardwareverifikation in der Industrie (II) / Formale Methoden

Jürgen Ruf / IBM Labor Böblingen
Thomas Kropf / Bosch Leonberg

Aktuelles

Am 29. Januar fällt die Vorlesung aus
Ich wünsche allen ein gutes und erfolgreiches neues Jahr 2004
Die Folien vom 20. November gibts jetzt auch als pdf (für die, die Probleme mit dem ps hatten)
Dirk wird leider keine Vorlesungen mehr halten :-(
Am 13. November entfällt die Vorlesung !!!!
Am 6. November beginnt die Vorlesung erst um 17:30 !!!!
Die Vorlesung wird entgegen der Ankündigung im VVV wöchtentlich mit 2 SWS abgehalten

Beschreibung

Die Vorlesungen Hardwareverifikation in der Industrie I und II bilden einen Vorlesungszyklus, mit sich ergänzenden Inhalten, wobei die Vorlesungen nicht aufeinander aufbauen und auch unabhängig voneinander gehört und geprüft werden können. Alle Dozenten haben einschlägige Erfahrungen im Entwurf und der Verifikation von Systemen im industriellen Umfeld (IBM/Bosch).
Durch den Einsatz moderner Mikroelektronik in sicherheitskritischen Anwendungen (Flug-/Raumfahrt, KFZ-Technik, Produktionssteuerung) steigen die Anforderungen an die Korrektheit der eingesetzten Komponenten unaufhörlich. Um diesen Anforderungen gerecht zu werden, muß im industriellen Entwurfszyklus der Aufwand zur Verifikation dieser Komponenten ständig gesteigert werden (bereits heute gehen bis zu 80% des Entwicklungsaufwandes zu Lasten der Verifikation)
Da mit simulationsbasierten Techniken eine erschöpfende Fehlersuche in der komplexen Hardwarebeschreibung nicht mehr möglich ist, werden immer häufiger formale Beweismethoden hinzugenommen. Um diese Techniken auch für einen Entwerfer nutzbar zu machen, werden insbesondere automatische Beweistechniken bevorzugt.
In dieser Vorlesung werden die Grundlagen für automatische Hardwareverifikation beschrieben:

Beschreibung der Hardware
formale Hardwaremodelle
Datenstrukturen zur Repräsentation (BDDs,...)

Außerdem werden wir die wichtigsten, in der Industrie eingesetzten Methoden besprechen:

Äquivalenzprüfung
Symbolische Modellprüfung/symbolische Simulation
Zeitbegrenzte Modellprüfung mit SAT-Methoden
semiformale Ansätze und kombinierte Techniken

Ort und Zeit

Die Vorlesung findet während des Wintersemesters 2003/2004
donnerstags um 17:00 bis 18:30 Uhr
im kleinen Hörsaal Sand 6 statt.

Prüfung

Pruefungsfach: Technische Informatik
Umfang: 2 SWS
Turnus: unregelmäßig

Termine

16.10.2003	Einleitung	*Thomas Kropf*
23.10.2003	BDDs	*Jürgen Ruf*
30.10.2003	Equivalence checking	*Dirk Hoffmann*
6.11.2003	Endliche Automaten	*Jürgen Ruf*
20.11.2003	Symbolic state space traversal [PDF]	*Jürgen Ruf*
27.11.2003	Circuit rectification	*Dirk Hoffmann*
4.12.2003	Temporallogik, CTL Modellprüfung	*Thomas Kropf*
11.12.2003	Sugar	*Jürgen Ruf*
08.1.2004	Temporal Expressions Symbolic Simulation [ps 5MB] Symbolic Simulation [pdf 14MB] Bounded Model Checking [ps] Bounded Model Checking [pdf]	*Jürgen Ruf*
15.1.2004	RuleBase SemiFormalVerification at IBM	*Jürgen Ruf*
22.1.2004	HOL	*Thomas Kropf*
5.2.2004	---	*Thomas Kropf*
12.2.2004	---	*Thomas Kropf*

Literatur

Thomas Kropf, Introduction to formal Hardware Verification