Achtung: Orts- und Zeitänderung ab 17. Mai 2011 Di 14.30-17:00 Uhr, Bibliothek, Lehrstuhl 12, Tennenlohe (Vorlesung und Übung)
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:
Modellierung digitaler Systeme
Unterschiede formaler und simulationsbasierter Verifikationsmethoden
Äquivalenzvergleich
Formale und simulationsbasierte Eigenschaftsprüfung
Assertions
Verifikation arithmetischer Schaltungen
Unterlagen:
Vorlesungsfolien (Zugriff nur innerhalb des Uni-Netzwerks möglich)
