Nach einem allgemeinen Überblick über das Gebiet des VLSI-Entwurfs werden wird uns auf das Teilgebiet der Hardware-Verifikation konzentrieren.

Verifikation beschäftigt sich (in vielen verschiedenen Ausprägungen) mit der Frage, wie die Korrektheit eines Entwurfs im Vergleich mit der gegebenen Spezifikation nachgewiesen werden kann.

Traditionell wurde die Verifikation oft durch Simulation von "einigen" funktionalen Mustern "gelöst". Spätestens seit dem öffentlichen Aufsehen, das der sogenannte "Pentium-Bug" erregt hat, ist die Fragwürdigkeit eines solchen Vorgehens offensichtlich: Eine formale Verifikation, d.h. ein Korrektheitsbeweis, gewinnt auch für die industrielle Praxis immer mehr an Bedeutung.

In dieser Vorlesung werden verschiedene existierende Techniken zur Harwareverifikation vorgestellt wie z.B. Binary Decision Diagrams, Word-level Decision Diagrams, symbolische Methoden zum Äquivalenznachweis für sequentielle Schaltungen, Model Checking zum Nachweis von Eigenschaften von Schaltungen etc.

Literatur zur Veranstaltung

• Kropf, Thomas, "Introduction to Formal Hardware Verification", Springer, 1999, ISBN 3-540-65445-3
• Drechsler, Rolf und Becker, Bernd, "Graphenbasierte Funktionsdarstellung: Boolesche und Pseudo-boolesche Funktionen", Teubner, 1998, ISBN 3-519-02149-8, Frei91:CB/6.0/22 
• Molitor, Paul und Scholl, Christoph, "Datenstrukturen und effiziente Algorithmen für die Logiksynthese kombinatorischer Schaltungenn", Teubner, 1999, ISBN 3-519-02945-6
• Kropf, Thomas(Ed.), "Formal Hardware Verification", Springer, 1997, ISBN 3-540-63475-4
• Originalarbeiten