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 hdl:20.500.11880/25765 http://dx.doi.org/10.22028/D291-25709 |
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 | Size | Format | |
---|---|---|---|---|
DanielKroening_ProfDrWolfgangJPaul.pdf | 1,37 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.