Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500)

Der Artikel stellt ein System zur weitgehend automatischen Verifikation von Schaltkreisen auf der Register-Transfer-Ebene vor. Dieses besteht im wesentlichen aus den Komponenten MEPHISTO, das auf das Beweissystem HOL für eine Logik höherer Stufe aufgesetzt ist, und FAUST, einem automatischen Beweissystem für eine Logik erster Stufe. In der Einleitung wird nach der Motivation und einer Einführung in die Problemstellung eine übersichtliche Gliederung der verschiedenen bekannten Methoden gegeben. Dabei werden Stärken und Schwächen dieser Ansätze diskutiert, womit die Autoren ihre Strategie begründen. Kapitel 2 enthält einen knappen Überblick über das HOL-Beweissystem und beschreibt kurz die Beweisstrategie des vorgestellten, darauf aufbauenden Systems, wobei insbesondere die Verteilung der Gesamtaufgabe auf die beiden Werkzeuge MEPHISTO und FAUST dargestellt wird. In Kapitel 3 werden dann die zugehörigen Beweisschritte vertieft erläutert. Nach der Definition einer eingeschränkten Logik höherer Stufe, die an die Problemstellung angepaßt ist, werden die Beschreibung von Spezifikation und Implementierung sowie Normalformen und Vereinfachungsmöglichkeiten für Ausdrücke dieser Logik vorgestellt. Weiterhin wird die gesamte Systemarchitektur erläutert, d.h. die Einbettung der Werkzeuge in eine CAD-Entwurfsumgebung. Die beiden nächsten Kapitel gehen genauer auf das Werkzeug FAUST ein. Während Kapitel 4 für den zugrundeliegenden Kalkül sowohl Vollständigkeit als auch Korrektheit zeigt, d.h. daß eine Formel genau dann gültig ist, wenn es einen Beweisbaum für sie gibt, behandelt Kapitel 5 Aspekte der Implementierung. Insbesondere wird der auf einer vorher festgelegten Reihenfolge von Regelanwendungen basierende Algorithmus zur Konstruktion eines Beweisbaums skizziert. Weiterhin werden Optimierungen und die Einbettung in HOL beschrieben. Kapitel 6 zeigt experimentelle Ergebnisse, bevor in Kapitel 7 die Zusammenfassung und ein Ausblick auf sich anschließende Fragestellungen erfolgen. Der umfangreiche Anhang enthält die Spezifikation von Basiskomponenten, eine Tafel zur HOL-Syntax, die in FAUST implementierte Regelmenge, eine große Zahl einfacher Schaltkreis-Beispiele, das Listing einer Sitzung zur Verifikation einer solchen Schaltung, sowie ein Beispiel, das die Anwendbarkeit des Systems zur Entdeckung von Hazards in Schaltkreisen zeigt. Der Artikel richtet sich gleichermaßen an CAD-Entwerfer und Entwickler von Beweissystemen. Während die ersten Kapitel einen Überblick über die zu lösenden Aufgaben und die Anwendung des Systems vermitteln, sind Kapitel 4 und 5 aufgrund der vorgestellten Interna des Systems für Anwender von geringerem Interesse.