Verifikation digitaler Systeme

Die heute entwickelten VLSI-Bausteine und die aus ihnen aufgebauten digitalen Systeme zählen zu den komplexesten Gebilden, die technisch überhaupt je realisiert wurden. Sie sind aus sehr vielen (hunderttausenden) Teilen aufgebaut. Ihr Entwurf steht wegen der hohen Folgekosten von Entwurfsfehlern zugleich unter dem Zwang, daß er fehlerfrei sein muß; ein Versuchsaufbau von VLSI-Bausteinen ist ausgeschlossen.

Mit der zunehmenden Nutzung integrierter Bausteine auch bei sicherheitskritischen Anwendungen ist die Forderung, daß diese Bausteine und die aus ihnen aufgebauten Hardwaresysteme ohne Entwurfsfehler seien, immer dringender geworden; schließlich steuern integrierte Bausteine Flugzeuge, werden in Banken und auf Intensivstationen eingesetzt, usf.

Ein mathematisches Modell eines physikalischen Hardwaresystems besteht aus einer Reihe mathematischer Objekte, z.B. aus Zahlen, Funktionen, Relationen usw. Die Eigenschaften des mathematischen Modells stehen stellvertretend für die des physikalischen Systems (Abb. 2.1).

Ein sehr allgemeines Modellierungskonzept des Verhaltens eines physikalischen Systems ist durch die Vorstellung gegeben, daß an ihm Beobachtungen oder Messungen in Abhängigkeit von der Zeit vorgenommen und durch ein geeignetes mathematisches Modell dargestellt werden. Messungen in Abhängigkeit von der Zeit werden durch Zeitfunktionen repräsentiert. Die Abb. 3.1 zeigt das Beispiel eines Kondensators. u(t) und i(t) sind Zeitfunktionen und stellen die in Abhängigkeit von der Zeit meßbare Spannung bzw. den Strom dar. Der Zusammenhang zwischen Strom und Spannung ist durch eine Differentialgleichung, d.h. eine Formel der Analysis festgelegt.

Werden die wesentlichen Eigenschaften eines Verhaltensmodells M durch eine Reihe von Formeln der Prädikatenlogik A₁, ..., A _n in textlicher Form charakterisiert, dann erlauben es die Schlußregeln der Prädikatenlogik, durch rein syntaktische Transformationen weitere, ebenfalls in M gültige Formeln abzuleiten. Dies wird mit dem Symbol “⊢” bezeichnet (Abb. 5.1).

Die Axiomatisierung von Programmierspachen [Hoa69, Dij76, Gri81] ist eine Methode, die Bedeutung von Programmen dadurch zu erklären, daß Anweisungen eines Programms in einer Programmiersprache in Formeln der Prädikatenlogik transformiert werden; die Schlußregeln der Prädikatenlogik erlauben dann das formale Argumentieren über Programme. Prinzipiell bedeutet daher die Axiomatisierung die Transformation eines Textes in einer formalen Sprache in eine formale Sprache der Prädikatenlogik; die entstehenden Formeln werden als Axiome in eine Theorie der Prädikatenlogik (Abschnitt 5.5) aufgenommen.

Nach Abschnitt 3.3 bedeutet statisches Verhalten eines Systems, daß die Ausgänge des Systems zu einem Zeitpunkt t eindeutig durch die Eingänge ebenfalls zum Zeitpunkt t bestimmt sind. Im Beispiel der Abb. 8.1 sind etwa a(t) und b(t) die Werte an den Eingängen eines Und-Gatters, die den Ausgangswert x(t) eindeutig festlegen.

Bei einem System mit transitionalem Verhalten ist der Ausgang zu einem Zeitpunkt t eindeutig durch den Eingang und den Ausgang zum vorherigen Zeitpunkt t-1 bestimmt (Abschnitt 3.3). Ein Beispiel für derartiges Verhalten sind die Zustandstabellen endlicher Automaten.

Mit den im vorigen Kapitel eingeführten ert-Beschreibungen können Zustandsänderungen unter zeitlich sich wechselseitig ausschließenden Bedingungen spezifiziert werden. Sie entsprechen den Darstellungen des Verhaltens endlicher Automaten durch Zustandsdiagramme.

In den vorangegangenen Kapiteln wurden Konstrukte der HWBS SMAX zur Modellierung von Verhalten betrachtet, das nach der Klassifikation von Abschnitt 3.3 statisch oder transitional war. Die Kenntnis des gegenwärtigen bzw. vorherigen Zustands reichte bereits aus, um den Ausgang eines Systems eindeutig zu bestimmen.

Das Grundelement von Switch-Level Beschreibungen ([Bry84, Hay82] ist der MOS-Transistor als bidirektionaler Schalter mit drei Anschlüssen, Gate, Source und Drain genannt. Ein einfaches zweiwertiges Modell eines NMOS-Transistors ist dadurch gegeben, daß der Wert H an Gate bewirkt, daß Source und Drain denselben Wert annehmen (Abb. 12.1). Man beachte, daß das Verhalten eines MOS-Transistors durch die Angabe einer Gleichheit, d.h. durch ein Prädikat definiert wird, im Gegensatz zur Modellierung etwa eines Gatters durch eine boolesche Funktion.

In den vorigen Kapiteln wurde an einigen Beispielen das Konzept der Axiomatisierung von Aktivitätsaufrufen diskutiert. Aufgabe von Aktivitätsaufrufen ist es, die Zeitfunktionen der privaten Träger (Definition 6.3) einer Beschreibung zu definieren.

In den vorangegangenen Kapiteln wurde die Aufgabe gelöst, die Modellvorstellungen einer Reihe von Abstraktionsebenen zu definieren und einer formalen Argumentation zugänglich zu machen. Dabei wurde auch die Schwerfälligkeit formaler Argumentationsweisen deutlich. Da nicht erwartet werden kann, ein komplexes System in einem Schritt verifizieren zu können, muß geklärt werden, wie die Entwurfsaufgabe, ein System zu verifizieren, in eine Reihe kleiner, beherrschbarer Verifikationsschritte unterteilt werden kann.

Der im vorigen Kapitel behandelte Fall der Erweiterung ist für eine Hardware-Spezifikationstechnik (s. Abb. 16.1) insofern einfach, als die grundlegenden Modellvorstellungen und damit die Konzepte der Zeit und der Werte übereinstimmen.

Die simulationsgestützte Verifikation eines Teils eines komplexen Systems ist eine sehr schwierige Aufgabe; ein System wird meist als Ganzes simuliert. Der Grund hierfür ist die problematische Entwicklung der Simulationsstimuli für einen aus einem Gesamtsystem herausgelösten Teil; die Stimuli stehen dann nämlich stellvertretend für das Verhalten des restlichen Systems und es ist unklar, inwieweit tatsächliches und durch die Simulationsstimuli unterstelltes Verhalten übereinstimmen. Versuche, nur Teile eines Systems zu simulieren, sind regelmäßig fehlgeschlagen; der Zwang, Systeme als Ganzes simulieren zu müssen, hat zur Entwicklung immer leistungsfähigerer Simulatoren bis hin zur Unterstützung durch spezielle Hardware geführt.

In den Kapiteln 16 und 17 wurde gezeigt, daß die korrekte Implementierung der Funktion einer Beschreibung oft davon abhängt, daß die Umgebung der Beschreibung eine Reihe von Schnittstellenbedingungen (Definition 13.2) einhält. Ein bekanntes Beispiel hierfür sind die Setup- und Haltezeit-Bedingungen von Flipflopbausteinen. Die gewünschte Funktion dieser Bausteine, nämlich die sichere Speicherung in Abhängigkeit von einem Taktsignal, ist nur dann garantiert, wenn Daten- und Takt-Eingangssignale die erwähnten Bedingungen einhalten. Andernfalls kann unerwünschtes Verhalten, etwa metastabile Zustände auftreten. Das Beispiel zeigt, daß Schnittstellenbedingungen relativ zu einer gewünschten Funktion verstanden werden müssen — das Gatternetz beispielsweise, das das Flipflopverhalten realisieren soll, reagiert ja auch irgendwie, wenn die Setup- und Haltezeit-Bedingungen nicht eingehalten werden.

Die Grundaufgabe der Timing-Verifikation läßt sich wie folgt formulieren: Gegeben seien die internen Zeitbedingungen eines Systems, d.h. die Zeitbedingungen der Teile eines Systems. Wie lauten die externen Zeitbedingungen an der Schnittstelle des Systems, die eingehalten werden müssen, um die internen Zeitbedingungen zu erfüllen?

Im letzten Kapitel soll kurz auf die prinzipielle Struktur von Verifikations-Werkzeugen eingegangen werden. Das bei der Entwicklung eines derartigen Werkzeuges zu berücksichtigende Wissen kann nach Abb. 22.1 drei verschiedenen Kategorien zugeordnet werden: