5.9 Formale Verifikation
317
Checker. Sie werden verwendet, um zu entscheiden, ob zwei Darstellungen äquivalent sind oder nicht (es gibt keine unsicheren Fälle). Beispielsweise kann eine
Darstellung den Gattern einer realen Schaltung entsprechen, während die andere
der Spezifikation entspricht. Der Beweis der Äquivalenz der beiden Darstellungen
beweist dann die Korrektheit aller durchgeführter Transformationen (beispielsweise Energie- oder Laufzeitoptimierungen). Tautologie-Checker können häufig
mit Systemen umgehen, die für eine vollständige simulationsbasierte Validierung zu groß sind. Der Hauptgrund für die Mächtigkeit von neueren TautologieCheckern liegt in der Verwendung von binären Entscheidungsdiagrammen (engl.
Binary Decision Diagrams (BDDs)) [570]. Die Komplexität eines BDD-basierten Äquivalenz-Checkers für Boolesche Funktionen wächst linear mit der Anzahl
der Knoten des BDDs. Die Anzahl der Knoten eines BDDs kann zwar exponentiell mit der Anzahl der Variablen wachsen, aber für viele praktisch relevante
Funktionen sind BDDs kompakt, sodass ein effizienter Vergleich möglich ist12.
Im Gegensatz dazu ist die Äquivalenzprüfung von Funktionen in einer DNFDarstellung (also als Summe von Produkten) NP-hart. Auf BDDs basierende
Äquivalenz-Checker haben daher für diese Anwendung Simulatoren verdrängt,
sie können mit Schaltungen umgehen, die aus mehreren Millionen Transistoren
bestehen.
• Die Prädikatenlogik erster Stufe beinhaltet die Quantifizierung mithilfe der
Existenz- (∃) und All-Quantoren (∀). Ein gewisses Maß an Automatisierung für
die Verifikation durch Prädikatenlogik erster Stufe ist möglich. Da diese Logik
im Allgemeinen nicht entscheidbar ist, können unsichere Fälle auftreten.
• Prädikatenlogik höherer Stufe (engl. Higher Order Logic (HOL)): Prädikatenlogik höherer Stufe erlaubt es, Funktionen so wie andere Objekte zu manipulieren
[424]. Bei Verwendung von Logik höherer Ordnung ist die Automatisierung von
Beweisen schwierig.
Die Aussagenlogik kann verwendet werden, um zustandslose Logiknetze zu verifizieren, sie kann aber nicht direkt endliche Automaten modellieren. Für kurze
Eingabefolgen kann es ausreichen, die Rückkopplung des Automaten aufzutrennen
und im Endeffekt mehrere Kopien dieses Automaten zu betrachten, von denen jede die Auswirkung eines Eingabemusters wiedergibt. Diese Methode ist aber nicht
sinnvoll auf längere Eingabefolgen anwendbar.
Solche Folgen können mittels Modellüberprüfung (engl. model checking) verarbeitet werden. Beim model checking erhält das Verifikationswerkzeug zwei Eingaben:
1. Ein Modell des zu verifizierenden Systems und
2. die zu überprüfenden Eigenschaften.
Zustände können mit ∃ und ∀ quantisiert werden, Zahlen jedoch nicht. Verifikationswerkzeuge können die Eigenschaften beweisen oder widerlegen. Für letzteren
Fall können sie ein Gegenbeispiel angeben. Model checking lässt sich leichter als
12 Die Multiplikation ist eine prominente Ausnahme [285].
317
Checker. Sie werden verwendet, um zu entscheiden, ob zwei Darstellungen äquivalent sind oder nicht (es gibt keine unsicheren Fälle). Beispielsweise kann eine
Darstellung den Gattern einer realen Schaltung entsprechen, während die andere
der Spezifikation entspricht. Der Beweis der Äquivalenz der beiden Darstellungen
beweist dann die Korrektheit aller durchgeführter Transformationen (beispielsweise Energie- oder Laufzeitoptimierungen). Tautologie-Checker können häufig
mit Systemen umgehen, die für eine vollständige simulationsbasierte Validierung zu groß sind. Der Hauptgrund für die Mächtigkeit von neueren TautologieCheckern liegt in der Verwendung von binären Entscheidungsdiagrammen (engl.
Binary Decision Diagrams (BDDs)) [570]. Die Komplexität eines BDD-basierten Äquivalenz-Checkers für Boolesche Funktionen wächst linear mit der Anzahl
der Knoten des BDDs. Die Anzahl der Knoten eines BDDs kann zwar exponentiell mit der Anzahl der Variablen wachsen, aber für viele praktisch relevante
Funktionen sind BDDs kompakt, sodass ein effizienter Vergleich möglich ist12.
Im Gegensatz dazu ist die Äquivalenzprüfung von Funktionen in einer DNFDarstellung (also als Summe von Produkten) NP-hart. Auf BDDs basierende
Äquivalenz-Checker haben daher für diese Anwendung Simulatoren verdrängt,
sie können mit Schaltungen umgehen, die aus mehreren Millionen Transistoren
bestehen.
• Die Prädikatenlogik erster Stufe beinhaltet die Quantifizierung mithilfe der
Existenz- (∃) und All-Quantoren (∀). Ein gewisses Maß an Automatisierung für
die Verifikation durch Prädikatenlogik erster Stufe ist möglich. Da diese Logik
im Allgemeinen nicht entscheidbar ist, können unsichere Fälle auftreten.
• Prädikatenlogik höherer Stufe (engl. Higher Order Logic (HOL)): Prädikatenlogik höherer Stufe erlaubt es, Funktionen so wie andere Objekte zu manipulieren
[424]. Bei Verwendung von Logik höherer Ordnung ist die Automatisierung von
Beweisen schwierig.
Die Aussagenlogik kann verwendet werden, um zustandslose Logiknetze zu verifizieren, sie kann aber nicht direkt endliche Automaten modellieren. Für kurze
Eingabefolgen kann es ausreichen, die Rückkopplung des Automaten aufzutrennen
und im Endeffekt mehrere Kopien dieses Automaten zu betrachten, von denen jede die Auswirkung eines Eingabemusters wiedergibt. Diese Methode ist aber nicht
sinnvoll auf längere Eingabefolgen anwendbar.
Solche Folgen können mittels Modellüberprüfung (engl. model checking) verarbeitet werden. Beim model checking erhält das Verifikationswerkzeug zwei Eingaben:
1. Ein Modell des zu verifizierenden Systems und
2. die zu überprüfenden Eigenschaften.
Zustände können mit ∃ und ∀ quantisiert werden, Zahlen jedoch nicht. Verifikationswerkzeuge können die Eigenschaften beweisen oder widerlegen. Für letzteren
Fall können sie ein Gegenbeispiel angeben. Model checking lässt sich leichter als
12 Die Multiplikation ist eine prominente Ausnahme [285].