Die Korrektheit eines digitalen Systems vollständig nachzuweisen - dieses Problem, das von großem praktischen Interesse ist, wirft eine Reihe grund legender Fragen der Modellierung von Hardware, der Entwicklung geeig neter Repräsentationen, der Möglichkeit formalen Argurnentierens und der technischen Realisierbarkeit von Verifikationswerkzeugen auf. Das vorliegende Buch gibt eine Einführung für diejenigen, die sich mit dem Gebiet der Hardwareverifikation vertraut machen wollen. Während ein Buch über dieses Thema - insbesondere auf Deutsch verfaßt - vor einigen Jahren noch etwas fast missionarisches gehabt hätte, findet das Gebiet inzwischen verbreitetes Interesse, was sich in einer zunehmenden Anzahl an Konferen zen und Veröffentlichungen wiederspiegelt. Dieses Interesse hat seine Ur sache einmal sicherlich in einem gesteigerten Problembewußtsein, daß man sich eben bei VLSI-Bausteinen keine Entwurfsfehler mehr leisten kann. Zum anderen wird immer mehr erkannt, daß das Problem der Verifikation fun damental ist für den gesamten Bereich des Hardwareentwurfs. Das Buch ist entstanden aus meiner Habilitationsschrift, aus Materialien zu einer Vorlesung "Entwurfsmethodik für komplexe digitale Systeme", die ich an der Technischen Hochschule Darmstadt von 1985 bis 1990 hielt, so wie aus einer Reihe englischsprachiger Berichte, die ich zum Zwecke der Selbstverständigung über das Gebiet geschrieben habe. Mein besonderer Dank gilt Prof. R. Piloty für die jahrelange Förderung mei ner Arbeit. Er bot mir die Möglichkeit, meine Ideen über die Verifikation digitaler Systeme während meiner Zeit als Mitarbeiter und später als Habi litand am Institut für Datentechnik der Technischen Hochschule Darmstadt zu entwickeln.
Die Korrektheit eines digitalen Systems vollständig nachzuweisen - dieses Problem, das von großem praktischen Interesse ist, wirft eine Reihe grund legender Fragen der Modellierung von Hardware, der Entwicklung geeig neter Repräsentationen, der Möglichkeit formalen Argurnentierens und der technischen Realisierbarkeit von Verifikationswerkzeugen auf. Das vorliegende Buch gibt eine Einführung für diejenigen, die sich mit dem Gebiet der Hardwareverifikation vertraut machen wollen. Während ein Buch über dieses Thema - insbesondere auf Deutsch verfaßt - vor einigen Jahren noch etwas fast missionarisches gehabt hätte, findet das Gebiet inzwischen verbreitetes Interesse, was sich in einer zunehmenden Anzahl an Konferen zen und Veröffentlichungen wiederspiegelt. Dieses Interesse hat seine Ur sache einmal sicherlich in einem gesteigerten Problembewußtsein, daß man sich eben bei VLSI-Bausteinen keine Entwurfsfehler mehr leisten kann. Zum anderen wird immer mehr erkannt, daß das Problem der Verifikation fun damental ist für den gesamten Bereich des Hardwareentwurfs. Das Buch ist entstanden aus meiner Habilitationsschrift, aus Materialien zu einer Vorlesung "Entwurfsmethodik für komplexe digitale Systeme", die ich an der Technischen Hochschule Darmstadt von 1985 bis 1990 hielt, so wie aus einer Reihe englischsprachiger Berichte, die ich zum Zwecke der Selbstverständigung über das Gebiet geschrieben habe. Mein besonderer Dank gilt Prof. R. Piloty für die jahrelange Förderung mei ner Arbeit. Er bot mir die Möglichkeit, meine Ideen über die Verifikation digitaler Systeme während meiner Zeit als Mitarbeiter und später als Habi litand am Institut für Datentechnik der Technischen Hochschule Darmstadt zu entwickeln.
Inhaltsverzeichnis
I: Grundlagen.- 1 Entwurfskorrektheit.- 2 Begriff der Abstraktionsebene.- 3 Modellierung von Verhalten.- 4 Sprachen der Prädikatenlogik.- 5 Formale Systeme der Prädikatenlogik.- II: Elementare Verifikationstechniken für Hardwarebeschreibungen.- 6 Hardwarebeschreibungen.- 7 Logikverifikation.- 8 Statische Beschreibungen.- 9 Transitionale Beschreibungen.- 10 Kombiniert statisch/transitionale Beschreibungen.- 11 Beschreibungen mit Vielfach-Verzögerungen.- 12 Switch-Level Beschreibungen.- 13 Strukturbeschreibungen.- III: Entwurfsmethodik.- 14 Strukturierte Entwurfsmethoden.- 15 Erweiterungen von Beschreibungen.- 16 Interpretierbare Beschreibungen.- 17 Zeitliche Abstraktion.- 18 Äquivalenz von Beschreibungen.- 19 Verifikation von Teilen.- 20 Horizontale Verifikation.- 21 Timing-Verifikation.- 22 Struktur von Verifikations-Werkzeugen.- Anhang: Beschreibung eines Divisionswerks auf vier Abstraktionsebenen.
