Inhaltsangabe
Der FM 8501 Mikroprozessor wurde als generischer Mikroprozessor erfunden, der einem PDP-11 ähnelt. Die Hauptidee der Bemühungen des FM 8501 war zu sehen, ob es möglich war, die Spezifikation auf Benutzerebene und die Design-Implementierung mit einer formalen Logik, der Boyer-Moore-Logik, auszudrücken. Dieser Ansatz ermöglichte einen vollständigen mechanisch überprüften Beweis, dass die FM 8501-Implementierung ihre Spezifikation vollständig umsetzte. Das Implementierungsmodell für den FM 8501 war für industrielles Hardware-Design unzureichend, aber der Aufwand war ein wichtiger Schritt in der Entwicklung zur Designverifizierungsmethode, die jetzt vom Autor angewendet wird. Die Originalversion dieses Monographen wurde als Dissertation an der University of Texas in Austin unter der Beratung von R. Boyer und J. Moore eingereicht.
Die Inhaltsangabe kann sich auf eine andere Ausgabe dieses Titels beziehen.
