Verifikation digitaler Systeme

Dozent: Prof. Dr. Oliver Keszöcze

Modulbeschreibung:

Verifikation digitaler Systeme

Umfang/Stunden:

V2 + Ü2

Ort und Zeit der Vorlesung:

Die Vorlesung findet Donnerstags um 08:15Uhr statt. Die Übung findet direkt im Anschluss statt.

Die Vorlesung wird in Präsenz stattfinden! Es gelten die 3G Regeln!

Aktuelle Corona-Informationen finden sie hier.

 

Die Vorlesung findet in Raum 02.112-128 statt.

Der erste Vorlesung findet Donnerstag  den 21.10.2021 um 10:15Uhr statt, der Übungsbetrieb findet in der ersten Woche noch nicht statt. In den folgenden Wochen findet dann die Vorlesung um 8:15 statt und die Übung direkt im Anschluss.

Ort und Zeit der Übungen:

Die Übung findet Donnerstags um 10:15Uhr in Raum 02.112-128 statt.

Unterlagen (Folien, Übungen, sonstige Dateien):

Alle Unterlagen zur Vorlesung und Übung finden sich in StudOn.

Zielsetzung:

Schwerpunkt der Vorlesung ist die funktionale Verifikation digitaler Systeme unter Einsatz formaler Methoden und simulationsbasierter Verfahren.

Inhalt:

Für den Entwurf eines digitalen Systems werden heute in der Industrie ebenso viele Verifikationsingenieure wie Designer benötigt. Trotzdem beansprucht die Verifikation heute bereits 70%-80% der gesamten Entwurfszeit. Neben konventionellen Verifikationsverfahren wie der Simulation werden seit einigen Jahren so genannte „formale Verifikationsmethoden“ in heutigen Entwurfsflüssen eingesetzt. Der Umgang mit diesen Methoden stellt ein wichtiges neues Aufgabenfeld dar. Im Gegensatz zur Simulation beruht die formale Verifikation auf exakten mathematischen Methoden zum Nachweis funktionaler Systemeigenschaften. Dadurch können Entwurfsfehler frühzeitiger und mit höherer Zuverlässigkeit als bisher erkannt werden. Jedes System zur formalen Verifikation erfordert:

  • ein geeignetes Modell des zu verifizierenden Systems
  • eine Sprache zur Formulierung der zu verifizierenden Eigenschaften
  • eine Beweismethode.

Die Vorlesung behandelt diese drei Bereiche, vermittelt die grundlegenden Algorithmen und Konzepte moderner Werkzeuge für die formale und simulationsbasierte Verifikation digitaler Systeme und erläutert deren Einsatz in der industriellen Praxis. Im Einzelnen werden in dieser Vorlesung die folgenden Punkte behandelt:

  1. Modellierung digitaler Systeme
  2. Unterschiede formaler und simulationsbasierter Verifikationsmethoden
  3. Äquivalenzvergleich
  4. Formale und simulationsbasierte Eigenschaftsprüfung
  5. Assertions
  6. Verifikation arithmetischer Schaltungen