Sie sind hier: Startseite Lehre Vorlesung Verifikation digitaler …

Vorlesung Verifikation digitaler Schaltungen

Organisatorische Details

  • Art der Veranstaltung: Spezialvorlesung in den Bachelor- und Masterstudiengängen Informatik und ESE
  • ECTS-Punkte: 6
  • Voraussetzungen: Basiswissen in Technischer Informatik.
  • Verantwortlich: apl. Prof. Dr. Ralf Wimmer
  • Mitwirkung: MSc Leonore Winterer
  • Übungen: vorlesungsbegleitende Übungsbögen und -fragen auf freiwilliger Basis

 

Ablauf

Wir werden versuchen, die Veranstaltung hybrid anzubieten, d. h. sofern die 3G-Regelung (geimpft, genesen oder getestet) eingehalten wird, sind alle Studierenden eingeladen, an der Vorlesung in Präsenz teilzunehmen. Für alle anderen wird es eine Live-Übertragung per BigBlueButton geben.

Termine und Ort

Montag, 10-12: Vorlesung

Mittwoch, 10-12: Vorlesung und Übung im Wechsel

Raum: Gebäude 51, R 03 026

Inhalte

Da elektronische Komponenten in immer mehr Bereiche unseres Lebens Einzug gehalten haben und insbesondere in sicherheitskritischen Anwendungen eingesetzt werden, ist es von zentraler Bedeutung, ihre korrekte Funktionsweise sicherzustellen. Simulation und Test sind gängige Methoden, um offensichtliche Fehler zu finden. Randfälle und andere selten auftretende Fehler werden damit aber oft nicht gefunden; ebenso lässt sich damit die Fehlerfreiheit nicht zeigen.
Deshalb werden heutzutage in der Halbleiterindustrie formale Methoden eingesetzt, die systematisch Fehler suchen und auch die Fehlerfreiheit beweisen können.

In dieser Vorlesung werden Datenstrukturen und Methoden vorgestellt, die die Basis für die formale Veriikation von digitalen Schaltungen bilden: Binäre Entscheidungsdigramme, SAT-Solver, And-Inverter-Graphen. Darauf aufbauend werden symbolische Methoden für den Äquivalenzvergleich und die automatische Prüfung von Eigenschaften digitaler Schaltungen vorgestellt, wie sie heutzutage täglich in der Industrie zum Einsatz kommen.

Der Einsatz dieser Methoden, insbesondere der Basistechniken und -datenstrukturen, ist dabei längst nicht (mehr) auf die Verifikation von Schaltungen beschränkt. SAT-Solver spielen beispielsweise auch in der künstlichen Intelligenz (Automated Reasoning, Knowledge Representation, Planning) eine wichtige Rolle.

Literatur

  • Kropf: "Introduction to Formal Hardware Verification" , Springer, 1999, ISBN 3-540-65445-3
  • Clarke, Grumberg, Peled, "Model Checking”, MIT Press 1999
  • Kropf (Ed.): "Formal Hardware Verification", Springer, 1997, ISBN 3-540-63475-4
  • Diverse Originalarbeiten

ILIAS E-Learning link

Weitere Details, aktuelle Nachrichten und Materialien zur Vorlesung werden über die ILIAS Plattform bereit gestellt:

Link

Die Zugangsdaten gibt es zu Beginn der Vorlesung vom Dozenten.