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 Verifikation der Korrektheitsbeweis.
Die formale Verifikation von Schaltkreisen wird oft in die Bereiche Äquivalenzvergleich und Modellprüfung gegliedert.Es sollen aus beiden Gebieten Verfahren vorgestellt werden. Wichtige Techniken hierbei sind die effiziente Repräsentation von Booleschen Funktionen (DDs) und Beweiser für Boolesche Erfüllbarkeit. 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.