Logo des Repositoriums
 

Formal verification of pipelined microprocessors

dc.contributor.authorKröning, Daniel
dc.contributor.editorWagner, Dorothea
dc.date.accessioned2017-09-22T20:41:12Z
dc.date.available2017-09-22T20:41:12Z
dc.date.issued2003
dc.description.abstractGegenstand 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.
dc.identifier.isbn978-3-88579-406-3
dc.identifier.pissn1617-5468
dc.identifier.urihttps://dl.gi.de/handle/20.500.12116/4448
dc.language.isode
dc.publisherGesellschaft für Informatik
dc.relation.ispartofAusgezeichnete Informatikdissertationen 2001
dc.relation.ispartofseriesLecture Notes in Informatics (LNI) - Dissertations, Volume D-2
dc.titleFormal verification of pipelined microprocessorsde
gi.citation.endPage80
gi.citation.publisherPlaceBonn
gi.citation.startPage71

Dateien

Originalbündel
1 - 1 von 1
Lade...
Vorschaubild
Name:
GI-Dissertations.02-7.pdf
Größe:
154.19 KB
Format:
Adobe Portable Document Format