Verifikation Digitaler Schaltungen / Verification of Digital Circuits - Wintersemester 21/22

Übersicht

Beschreibung

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.

Kommentar

Spezialvorlesung in den Bachelor- und Masterstudiengängen Informatik und ESE