Methoden der Verifikation 03-05-H-701.06
Veranstalter: Prof. Dr. Rolf Drechsler 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:
Äquivalenzvergleich und Modellprüfung.
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 finden sich hier
Hier ist die Literatursammlung
| 
