Informationen zur Vorlesung
"Formale Verifikation von Hardware" (WS 2002/03)
Verantwortlich Dr. Wolfgang Günther
Zeit
  • Tag 2: 8.11.2002, 13-16 ct
  • Tag 1: 18.10.2002, 13-16 ct
Weitere Termine nach Absprache
Ort SR 00-034, Geb. 051, Georges-Köhler-Allee
Beschreibung

Nach einem allgemeinen Überblick über das Gebiet des Hardware-Entwurfes werden wir uns auf das Gebiet der Hardware-Verifikation konzentrieren.

Verifikation beschäftigt sich (in vielen verschiedenen Ausprägungen) mit der Frage, wie die Korrektheit einer Schaltung nachgewiesen werden kann. Dabei interessiert zunächst die Korrektheit der Spezifikation, während später eine Korrektheit des Entwurfs im Vergleich zur gegebenen Spezifikation nachgewiesen werden soll.

Traditionell wurde die Verifikation oft durch Simulation von "einigen" funktionalen Mustern "gelöst". Spätestens seit dem öffentlichen Aufsehen, das der sogenannte "Pentium-Bug" erregt hat, ist die Fragwürdigkeit eines solchen Vorgehens offensichtlich: Eine formale Verifikation, d.h. ein Korrektheitsbeweis, ist auch in der industriellen Praxis nicht mehr wegzudenken.

In dieser Vorlesung werden zunächst verschiedene existierende Techniken zur Harwareverifikation vorgestellt, wie z.B. verschiedene Formen von Decision Diagrams, sowie SAT-Solver. Darauf aufsetzend werden Ansätze zum Äquivalenzvergleich sowie zum Überprüfen einer Spezifikation beschrieben.

Literatur zur Veranstaltung

  • G. Hachtel, F. Somenzi: Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, 1996.
  • Drechsler, Rolf und Becker, Bernd, "Graphenbasierte Funktionsdarstellung: Boolesche und Pseudo-boolesche Funktionen", Teubner, 1998, Frei91:CB/6.0/22 
  • Kropf, Thomas, " Introduction to Formal Hardware Verification", Springer, 1999.
Übungen Betreut von Marc Herbstritt, E-Mail: [herbstri@informatik.uni-freiburg.de]
Die Übungen finden generell am darauffolgenden Freitag einer Vorlesung statt in Raum 00-034 um 13:00Uhr.
Die Ausarbeitung zu den Übungen bitte per E-Mail an Marc Herbstritt schicken oder in Geb. 051 Raum 01-033 abgeben.

Übung 1 (15.11.2002), 13:00Uhr

Übung 2 (06.12.2002), 13:00Uhr

Übung 3 (18.12.2002), 13:30Uhr

Übung 4 (17.01.2003), 13:00Uhr
Vorlesungsfolien

Alle Foliensätze sind in PDF und PS (gepackt) verfügbar.


Tag 1 (18.10.2002)

Tag 2 (08.11.2002)

Tag 3 (29.11.2002)

Tag 4 (13.12.2002)

Tag 5 (10.1.2003)

  • Kombinatorische Verifikation (pdf)
  • Sequentielle Verifikation (pdf)
  • Aufgabenblatt 4 (Besprechung: 17.01.2003)

Tag 6 (24.1.2003)