Seminar SAT-basierte Verfahren im Schaltungsentwurf - Sommersemester 09
Übersicht
| Beschreibung |
Das Erfüllbarkeitsproblem der Aussagenlogik (SAT) beschreibt die Fragestellung, ob es für eine aussagenlogische Formel eine erfüllende Belegung gibt. Das Erfüllbarkeitsproblem Boolescher Formeln mit Quantoren (QBF) erweitert SAT um Quantifizierungen von Variablen und ermöglicht dadurch eine kompakte Darstellung vieler Problemstellungen. In den letzten Jahren konnte die Performanz von SAT- und QBF-Solvern drastisch gesteigert werden, so dass ein Einsatz dieser Techniken in vielen Gebieten möglich wurde. Ein sehr wichtiges Gebiet für die Anwendung SAT-basierter Techniken ist der Schaltungsentwurf. Dieses Themengebiet umfasst unter anderem folgende Anwendungen von SAT/QBF: - Logikoptimierung ("Wie kann eine gegebene Schaltung besser repräsentiert werden (z.B. weniger Gatter, geringere Verzögerungszeit, geringerer Energieverbrauch)?" ) - FPGA-Synthese ("Wie kann eine gegebene Schaltung mit einem FPGA realisiert werden?") - Diagnose ("Wie kann das Fehlverhalten der Gesamtschaltung durch lokal beschränkte Fehler erklärt werden?") - Verifikation von Arithmetik ("Wie kann ein SAT-Solver für die Verifikation von arithmetischen Schaltungen optimiert werden?") Das Seminar führt durch die Vorstellung von Originalarbeiten an den aktuellen Stand der Forschung auf diesem Gebiet heran und zeigt interessante Fragestellungen auf. Mögliche Themen sind unter Literatur aufgelistet. |
| Kommentar |
Das Seminar findet als Blockveranstaltung zum Semesterende statt. Die Vorbesprechung findet am Mittwoch, 29.4.09, 13:15 h im Hardwarepool (Geb. 51, Erdgeschoss) statt. |