Synthese und Verifikation Digitaler Systeme (SS96)


Dr.Michael Payer


Siemens AG
ZFE T SE 1
Otto-Hahn-Ring 6
81730 München
Tel. 089/636-45493;
email: Michael.Payer@zfe.siemens.de

Nr:

76336

Titel:

Synthese und Verifikation Digitaler Systeme

Einordnung in den Studienplan:

Die Vorlesung kann als Alternative/Ersatz zur Vorlesung Schaltwerkstheorie" (Informatik III / 3.1) belegt werden.
Sie dient zur Vertiefung der Wahlpflichtvorlesung "Automaten und Formale Sprachen".

Mögliche Prüfer:

Prof. Brauer, Prof. Esparza

Zeit und Ort:

Donnerstags, 8:30 - 10:00 Uhr, Hörsaal 0601

Beginn:

23. Mai 1996

Hörerkreis:

Hauptstudium

Voraussetzungen:

Außer den aus dem Grundstudium bekannten Themen sind keine weiteren Vorkenntnisse notwendig. Die Hörer sollten Vorkenntnisse in Compilerbau, Automaten- und Graphentheorie besitzen sowie die Grundbegriffe der Technischen Informatik kennen. Kenntnisse der Elektrotechnik sind nicht erforderlich.

Exkursion:

Bei Interesse wird eine Exkursion zur Siemens AG, München Perlach durchgeführt.

Skript:

Es gibt ein fertiges Skript, das während der Vorlesung verteilt wird.

Sprechstunde:

Eine Sprechstunde für inhaltliche und organisatorische Fragen wird angeboten. Sie findet in der Regel nach der Vorlesung, oder aber nach Vereinbarung (email oder Telephon) statt.

Zielsetzung:

Die Vorlesung im Umfang von 2 SWS soll den Hörern exemplarisch die industrielle Anwendung grundlegender Informatik-Konzepte aufzeigen. Als 'Vehikel' wird dazu ein Thema gewählt, das derzeit seinen Weg aus den Forschungslabors der Industrie (natürlich auch der Hochschulen) in den industriellen Einsatz findet, nämlich 'Synthese und Verifikation Digitaler Systeme'. Es kommt mir dabei ganz wesentlich auf die Anwendung von Konzepten, Paradigmen und Ideen an, die den Hörern in der Regel schon bekannt sein dürften; nicht jedoch darauf,

weiteres Spezialwissen ('die (n+1)te Theorie') zu präsentieren. Insbesondere soll den Hörern verdeutlicht werden, wie das bis dahin im Studium schon erworbene Wissen auch tatsächlich angewendet wird. Ein Ziel dabei ist, grundlegende Konzepte der Informatik in einen gemeinsamen Anwendungszusammenhang zu stellen. Dadurch soll den Hörern natürlich auch verdeutlicht werden, wie die einzelnen Teilgebiete der Informatik ineinandergreifen.

Was ist Synthese?

Im weitesten Sinne, die automatische Transformation von Verhaltensbeschreibungen in Strukturbeschreibungen. Die Verhaltensbeschreibung (oder Spezifikation) liegt dabei in der Regel in VHDL vor. VHDL ist eine simulierbare, eng an ADA angelehnte Hardware-Beschreibungssprache (mit parallelen Prozessen, etc.). Interessant dabei ist, daß eine solche Beschreibung in VHDL zu einer auf dem Rechner ausführbaren Spezifikation wird.

Was ist Verifikation?

1. Vollständige, d.h. 100%ige automatische Überprüfung, daß die Synthese korrekt abgelaufen ist.

2. Überprüfung der Spezifikation auf Korrektheit. Dabei werden ausgewählte Eigenschaften des spezifizierten Modells untersucht. Beispiele solcher Eigenschaften sind:

Inhalt:

Unter High-Level-Synthese versteht man die automatische Synthese einer Hardware-Strukturbeschreibung aus einer algorithmischen Verhaltensbeschreibung. Die so synthetisierte Strukurbeschreibung besteht aus einem Controller in Form eines endlichen Automaten und einem Datenpfad (Multiplexern, ALUs, Registern, Verbindungen, etc.), der die einzelnen Operationen realisiert.

Die wesentlichen Teilprobleme bei der Synthese sind das ``Scheduling'', also die Zuordnung von Operationen zu Kontrollschritten und die ``Allocation'', also die Abbildung von Konstrukten wie Variablen und Operatoren der Verhaltensbeschreibung auf den Datenpfad.

Im Unterschied zum traditionellen Übersetzerbau wird die Zielarchitektur ebenfalls synthetisiert. Ein wesentlicher Aspekt der Synthese ist das Auffinden einer Lösung, die ein ausgewogenes Verhältnis von Ausführungszeit und benötigten Hardware-Resourcen liefert (Design Space Exploration).

Aufgaben wie Scheduling und Allocation, aber auch gewisse Optimierungen, werden als Graphenprobleme formuliert. Soweit bekannt, werden effiziente exakte Lösungsverfahren vorgestellt, ansonsten die bekannten Heuristiken.

Wesentlich für die Akzeptanz von High-Level-Synthese-Systemen sind effiziente Verifikationsverfahren, mit denen die Äquivalenz von Spezifikation und synthetisierter Implementierung nachgewiesen werden kann; weiterhin Verfahren, mit denen Lebendigkeits- und Sicherheitseigenschaften der Spezifikation überprüft werden können (Model Checking). Die in letzter Zeit erzielten Fortschritte, insbesondere in der symbolischen Verifikation ``großer'' endlicher Automaten, werden behandelt.

Literatur:

1. Synthese

Camposano, R. and W. Wolf: "Trends in High-Level Synthesis", Kluwer Academic Publishers, 1991

Walker, R.A. and R. Camposano: "A Survey of High-Level Synthesis Systems", Kluwer Academic Publishers, 1991

Michel, P. and U. Lauther and P. Duzy: "The Synthesis Approach to Digital System Design", Kluwer Academic Publishers, 1992

Gajski, D. and N. Dutt: "High Level Synthesis", Kluwer Academic Publishers, 1993

2. Verifikation

K.L. McMillan: "Symbolic Model Checking", Kluwer Academic Publishers, 1993

Bryant, R.E.: "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams", ACM Computing Surveys, Sept. 1992, Vol.24, No.3, pp. 219-318

McFarland, M.C.: "Formal Verification of Sequential Hardware: A Tutorial", IEEE Trans. CAD, May 1993, Vol.12, No.5, pp. 633-654

3. Zeitschriften

- IEEE Transactions on Computer-Aided Design

- IEEE Transactions on Computers

- INTEGRATION the VLSI journal

- IEEE Design & Test of Computers

4. Konferenzen

- IEEE/ACM Design Automation Conference (DAC)

- IEEE/ACM International Conference on Computer Aided Design

- CHDL - Computer Hardware Description Languages and their Application

- European Design Automation Conference (EDAC)

- European Design Automation Conference with VHDL (EURO-DAC, EURO-VHDL)

- International Workshop on High-Level Synthesis


Zurück zu den Lehrveranstaltungen am Lehrstuhl Brauer