Verifikation Mikroprogrammierter Rechnerarchitekturen

Zusammenfassung

In Kapitel 3 haben wir sämtliche Hilfsmittel zur Verfügung gestellt, um einen hierarchischen Entwurf einer mikroprogrammierten Rechnerarchitektur formal zu beschreiben. Wir haben dargelegt, wie die Zielarchitektur des Entwurfs modular spezifiziert werden kann, haben die Technik der Einführung virtueller Zwischenarchitekturen zur Strukturierung des Entwurfes vorgestellt, und schließlich die Genauigkeit der Modellierung von Mikroarchitekturen in AADL diskutiert. Jeder Entwurfsschritt — jeder Obergang von einer höheren Ebene des Entwurfes zu einer näher zur Gastarchitektur hinführenden Ebene des Entwurfes — verlangt vom Entwerfer (neben der Beschreibung evtl. Zwischenarchitekturen) die Angabe einer Speicherabbildung - die die statischen Strukturen der Entwurfsebenen in Beziehung setzt — und eines implementierenden Programms, das das dynamische Verhalten der höheren Architekturebene nachbildet.