Dieses Seminar geht der Frage nach, wie die Korrektheit von Schaltungen nachgewiesen werden kann. Im Gegensatz zur Simulation von Schaltungen, deren Grenze z.B. durch den Pentium-Bug aufgezeigt wurde, ist das Ziel der formalen Verfikation der Korrektheitsbeweis.
Formale Verifikation lässt sich in zwei Bereiche einordnen:Es sollen aus beiden Gebieten Verfahren vorgestellt werden. Wichtige Techniken hierbei sind die effiziente Repräsentation von Booleschen Funktionen (DDs) und SAT-Solver. Im Rahmen der Verfahren zur Modellprüfung sollen temporale Logiken, wie z.B. CTL und LTL, betrachtet werden.
Ausgehend von einer kurzen Einführung über den Hardware-Entwurfprozess soll das Seminar bis zur aktuellen Forschung führen.
Termin und Ort nach Vereinbarung mit Prof. Dr. Rolf Drechsler.
Hinweise zum Seminar (pdf)
Schein (pdf)
| Thema |
Vortragende |
Ausarbeitung |
Folien |
| Der SAT-Beweiser CIRCUS | S. Meyer | ||
| Das Verifikationssystem GUIDO | Deng Zhou | ||
| Lösung von Integer Linear Programs | A. Kaib, O. Heid | ||
| Alles als Archiv | tgz |