Entwurf und Verifikation mikroprogrammierter Rechnerarchitekturen

Front Cover
Springer, 1987 - Computers - 327 pages
Dieses Buch stellt eine Methodik zum systematischen Entwurf korrekter Mikroprogramme vor. Behandelt werden sAmtliche Phasen der Firmwareentwicklung: das Erstellen einer formalen Beschreibung der Anforderungen, Techniken zur hierarchischen Organisation des Entwurfs, die Mikroprogrammierung in einer geeigneten hAheren Mikroprogrammiersprache, sowie formale Techniken zur AoeberprA1/4fung der Korrektheit des Entwurfs. Damit wird erstmals eine Firmwareverifikationsmethode vorgestellt, die sowohl fA1/4r beliebige Mikroarchitekturen einsetzbar ist als auch eine inkrementelle und modulare Verifikation des Entwurfs ermAglicht. Besonderes Gewicht wurde sowohl auf eine prAzise mathematische Durchdringung des Firmwareentwurfs als auch auf die praktische Anwendbarkeit der Entwurfsmethode gelegt. SAmtliche Konzepte und Techniken werden an Hand eines Emulationsbeispiels illustriert. Der Text enthAlt ein einfA1/4hrendes Kapitel, das sowohl die Grundbegriffe aus dem Bereich der Mikroprogrammierung als auch die verwendeten mathematischen Begriffsbildungen zusammenfaAt. Die beiden Hauptteile behandeln jeweils den Entwurf sowie die Verifikationsmethodik. In AnhAngen werden ausfA1/4hrliche Entwurfs- und Verifikationsbeispiele gegeben. Das Buch bietet sowohl dem Entwickler grAAerer Mikroprogramme als auch dem Ersteller von Firmwareentwicklungswerkzeugen einen geeigneten Rahmen zur Beherrschung der KomplexitAt von Mikroarchitekturen. FA1/4r Studenten der Informatik veranschaulicht der Text die Relevanz mathematischer Modellbildungen in einem konkreten Anwendungesgebiet.

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Einleitung
1
Grundbegriffe der Firmwareverifikation
7
Entwurf mikroprogrammierter Rechnerarchitekturen
26
Copyright

9 other sections not shown

Other editions - View all

Common terms and phrases

AADL Abbildung accu accumulator Adressierungsart Akkumulators Aktivierung Aktivierungsbedingung Architektur assert Ausführung Ausgabevariablen Auswertung auxiliary auxiliarysinks axiomatische Spezifikation Axiomatisierung base register address Befehls Befehlswortes Beispiel Beschreibung Beweisregel bit-slice blockdiagram buffer case Computer conflictcond(a,a Coroutine Datenkonflikte definiert defining equation Definition Deklaration denotation displacement Emulation Emulators endarray endcase endformat entry Entwurf exit faise Feld file-bank-select file-flag Firmware folgenden formale Funktion Gastarchitektur Generierung hex C6 hex FF Hilfsvariablen Hoare-Kalkül Implementierung instructionreg instructionword Instruktionswortes Interferenzfreiheit interrupt interrupt-on Kodierung konfliktfrei Korrektheit main makearray index memory memory[2 memory[A-register Menge Microcode Microprogramming Mikro Mikroarchitektur Mikrooperationen Mikroprogramm mikroprogrammierter modification-enable modify-register modify-register<5 Moduln move-data.accu move-data.index Nachbedingung NOVA operand-control Operation outputlocations parallelen Parameter pattern Phasenbedingung prädikatenlogische primary primaryfile programcounter Prozedur Rechnerarchitektur RWTH Aachen S*-Familie sämtliche Seiteneffekte semantics sequence sideeffects somit sources Speicher Speicherabbildung Speicherausdrücke Speicherelemente statischen statischen Analyse stcycle sub(main sub(time Substitution T-register test tion true post unfoldtype Vereinfachungsregeln Verifikation Verwendung Vorbedingung zero Zielarchitektur

Bibliographic information