Verifikation digitaler Systeme

Allgemeines

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

Lernziele

Die Studierenden können den Ablauf der Verifikation digitaler Systeme beschreiben und skizzieren. Sie können unterschiedliche Verifikationstechniken benennen, unterscheiden und deren Vor- und Nachteile aufzeigen. Sie wählen aus unterschiedlichen Verifikationstechniken unter Berücksichtigung von deren Mächtigkeit und Komplexität die richtige Methode aus, um ein gegebenes Problem zu lösen. Sie sind in der Lage Modelle digitaler Systeme zu konstruieren und Verifikationstechniken auf diese anzuwenden.

 

Leistungsnachweise und Notenbildung

Die Vergabe der Leistungspunkte erfolgt aufgrund des Bestehens der mündlichen Modulprüfung. Die Anmeldung zu dieser Prüfung setzt keinen Leistungsnachweis voraus. Die Modulnote entspricht dem Ergebnis der Modulprüfung.

 

Literatur

• Christian Haubelt und Jürgen Teich: Digitale Hardware/Software-Systeme: Spezifikation und Verifikation Springer, Berlin, 2010, ISBN 978-3642053559
• Thomas Kropf: Introduction to Formal Hardware Verification; Springer, Berlin, 1999, ISBN 3-540-65445-3
• William K. Lam: Hardware Design Verification: Simulation and Formal Method-Based Approaches, Prentice Hall Modern Semiconductor Design Series, 2005, ISBN 0-13-143347-4