Logo des Repositoriums
 
Textdokument

Formal verification of pipelined microprocessors

Lade...
Vorschaubild

Volltext URI

Dokumententyp

Zusatzinformation

Datum

2003

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Gesellschaft für Informatik

Zusammenfassung

Gegenstand der Dissertation ist die formale Verifikation von Mikroprozessoren mit Pipeline. Dies beinhaltet auch Prozessoren mit aktuellen Scheduling-Verfahren, wie den Tomasulo Scheduler und spekulativer Ausführung. Im Gegensatz zu weiten Teilen der bestehenden Literatur führen wir die Verifikation auf Gatter-Ebene durch. Des weitern beweisen wir sowohl Datenkonsistenz als auch eine obere Schranke für die Ausführungszeit. Die Beweise werden mit dem Theorem Beweissystem PVS verifiziert. Es werden sowohl in-order Maschinen als auch out-of-order Maschinen verifiziert. Zur Verifikation der in-order Maschinen erweitern wir die Stall Engine aus [MP00]. Wir entwickeln und implementieren ein Verfahren das die Transformation in die "pipelined machine" durchführt. Wir beschreiben eine generische Maschine, die die Spekulation auf beliebige Werte erlaubt. Wir verifizieren die Beweise für den Tomasulo Scheduler mit Reorder Buffer.

Beschreibung

Kröning, Daniel (2003): Formal verification of pipelined microprocessors. Ausgezeichnete Informatikdissertationen 2001. Bonn: Gesellschaft für Informatik. PISSN: 1617-5468. ISBN: 978-3-88579-406-3. pp. 71-80

Schlagwörter

Zitierform

DOI

Tags