Diese Arbeit baut auf einer formalen Methode von Börger und Mazzanti
 zur Verifikation des von Hennessy und Patterson definierten
 DLX-Mikroprozessors auf. Es wird die Beschreibung eines einfachen
 seriellen Modells des Prozessors mit der Beschreibung eines
 komplexeren parallelen Modells verglichen und gezeigt, daß beide die
 gleiche Funktionalität aufweisen.  Börger und Mazzanti verwenden dazu
 das Prinzip der abstrakten Zustandsmaschinen.

 In der hier vorliegenden Diplomarbeit wird gezeigt, wie die
 informelle Vorgehensweise von Börger und Mazzanti in einen
 mechanisierten und automatisierten Beweis umgesetzt werden kann. Die
 Definition und Verifikation der Maschinen wurde mit dem PVS
 Verifikationssystem ausgeführt. Es wurden die informellen
 Definitionen der seriellen DLX, der DLXp und der DLXdata
 Zustandsmaschinen von Börger und Mazzanti in die
 PVS-Spezifikationssprache übersetzt und geeignete
 Abbildungsfunktionen entwickelt, die es ermöglichen, diese Maschinen
 miteinander zu vergleichen. Für den Beweis, daß die serielle DLX und
 die parallele DLXp Maschine die gleiche Funktionalität aufweisen
 wurden geeignete PVS-Strategien entwickelt, die es ermöglichen diesen
 Beweis weitgehend vollautomatisch durchzuführen. Vor allem für die
 Teile des Beweises, die sehr lange Rechenzeiten benötigen, wird eine
 Strategie bereitgestellt, die diese Teile ohne Eingreifen des
 Benutzers abarbeitet.