Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25709
Titel: Formal verification of pipelined microprocessors
Sonstige Titel: Formale Verifikation von Mikroprozessoren mit Pipeline
Verfasser: Kröning, Daniel
Sprache: Englisch
Erscheinungsjahr: 2001
SWD-Schlagwörter: Mikroprozessor ; Pipeline-Verarbeitung ; Korrektheit ; Hardwareverifikation ; Formale Methode
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: Subject of this thesis is the formal verification of pipelined microprocessors. This includes processors with state of the art schedulers, such as the Tomasulo scheduler and speculation. In contrast to most of the literature, we verify synthesizable design at gate level. Furthermore, we prove both data consistency and liveness. We verify the proofs using the theorem proving system PVS. We verify both in-order and out-of-order machines. For verifying in-order machines, we extend the stall engine concept presented in [MP00]. We describe and implement an algorithm that does the transformation into a pipelined machine. We describe a generic machine that supports speculating on arbitraty values. We formally verify proofs for the Tomasulo scheduling algorithm with reorder buffer.
Gegenstand dieser Dissertation ist die formale Verifikation von Mikroprozessoren mit Pipeline. Dies beinhaltet auch Prozessoren mit aktuellen Scheduling-Verfahren wie den Tomasulo Scheduler und spekulativer Ausfuehrung. Im Gegensatz zu weiten Teilen der bestehenden Literatur fuehren wir die Verifikation auf Gatter-Ebene durch. Des weitern beweisen wir sowohl Datenkonsistenz als auch eine obere Schranke fuer die Ausfuehrungszeit. 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 beschreiben und Implementieren ein Verfahren das die Transformation in die "pipelined machine'; durchfuehrt. Wir beschreiben eine generische Maschine die Spekulation auf beliebige Werte erlaubt. Wir verifizieren die Beweise fuer den Tomasulo Scheduler mit Reorder Buffer.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-1985
hdl:20.500.11880/25765
http://dx.doi.org/10.22028/D291-25709
Erstgutachter: Wolfgang J. Paul
Tag der mündlichen Prüfung: 1-Jan-2001
SciDok-Publikation: 23-Apr-2004
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
DanielKroening_ProfDrWolfgangJPaul.pdf1,37 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.