Please use this identifier to cite or link to this item: doi:10.22028/D291-25709
Title: Formal verification of pipelined microprocessors
Other Titles: Formale Verifikation von Mikroprozessoren mit Pipeline
Author(s): Kröning, Daniel
Language: English
Year of Publication: 2001
SWD key words: Mikroprozessor ; Pipeline-Verarbeitung ; Korrektheit ; Hardwareverifikation ; Formale Methode
DDC notations: 004 Computer science, internet
Publikation type: Dissertation
Abstract: 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 to this record: urn:nbn:de:bsz:291-scidok-1985
Advisor: Wolfgang J. Paul
Date of oral examination: 1-Jan-2001
Date of registration: 23-Apr-2004
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
DanielKroening_ProfDrWolfgangJPaul.pdf1,37 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.