Übungen zur Vorlesung
Verifikation Digitaler Systeme
Aktuell:
Allgemeine Informationen
Die Übungen finden als Rechnerübungen statt. In den Übungsaufgaben lernen Sie ein industrielles Software-Werkzeug zur formalen Eigenschaftsprüfung ("property checking") für digitale Systeme kennen. Sie werden zunächst anhand kleinerer Übungsaufgaben mit der Benutzung und der Eingabesprache des Werkzeuges vertraut gemacht. Schließlich bearbeiten Sie eine etwas umfangreichere Verifikationsaufgabe, bei der Sie die funktionale Korrektheit eines einfachen RISC-Prozessors verifizieren sollen.
Voraussetzungen
Um die Inhalte der Vorlesung verstehen sowie die Übungsaufgaben bearbeiten zu können, benötigen Sie ausreichende Kenntnisse in Digitaltechnik. Sie sollten wissen, wie man kombinatorische und sequentielle Schaltungen modelliert und synthetisiert. Sie sollten mit Booleschen Funktionen und Grundbegriffen der Automatentheorie vertraut sein. Sie sollten z.B. wissen, was ein UND-Gatter, ein D-Flipflop, ein Zustandsdiagramm ist.
In den Übungsaufgaben werden Digitalschaltungen mit Hilfe der Hardware-Beschreibungssprache VHDL modelliert. Sie werden zwar nicht selbst Schaltungsmodelle in VHDL erstellen. Sie müssen die beschriebenen Modelle allerdings so gut verstehen, dass Sie gewünschte Eigenschaften der Systeme auf der Basis dieser VHDL-Modelle formulieren und verifizieren können. Dafür benötigen Sie Grundkenntnisse in VHDL, die Sie sich aber im Laufe des Semesters aneignen können.
Es gibt umfangreiche Literatur über VHDL, sowohl in Buchform als auch im Internet. Exemplarisch sei hier genannt:
- Peter J. Ashenden "The Designer's Guide to VHDL, 2nd Edition", Morgan Kaufmann Publishers, San Francisco, ISBN 1-55860-674-2.
- http://tams-www.informatik.uni-hamburg.de/vhdl
- "VHDL Cookbook" von Peter J. Ashenden, zum Download im Internet, z.B.http://tams-www.informatik.uni-hamburg.de/vhdl/doc/cookbook/VHDL-Cookbook.pdf
ACHTUNG: Nachteil: Dieses Buch deckt nur den älteren VHDL-87-Standard ab.
Orte und Zeiten
Die Übungen werden hauptsächlich als Rechnerübungen durchgeführt. Am Anfang des Semesters finden die Übungstermine jedoch für Vorbesprechungen und Einführung in die Thematik im Hörsaal statt. Dies wird jeweils vorher auf dieser Webseite bekanntgegeben.
| Hörsaalübung: Dienstags, 13:45 - 15:15 Uhr, G11-241 | |
Rechnerübung: Dienstags, 13:45 - 15:15 Uhr, Rechenzentrum Terminal-Pool II (34/251) |
Rechnerübung:
Im Rechenzentrum werden Arbeitsplätze für den oben angegebenen Zeitraum reserviert sein. An jedem Arbeitsplatz liegt ein Belegungsplan aus, in dem die Reservierung eingetragen ist.
Freies Üben:
Während der Öffnungszeiten des Rechenzentrums können Sie zu jeder Zeit an den Arbeitsplätzen arbeiten, sofern sie frei sind (Belegungsplan beachten!). Außerdem können Sie sich über das Internet mit Hilfe des Programms "secure shell", ssh, von außerhalb in das System einloggen und arbeiten.
Bei Fragen senden Sie bitte eine Email an Carlos Villarraga: villarraga@eit.uni-kl.de