Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25704
Titel: Formal verification of a fully IEEE compliant floating point unit
Verfasser: Jacobi, Christian
Sprache: Englisch
Erscheinungsjahr: 2002
SWD-Schlagwörter: Mikroprozessor ; Gleitkommarechnung ; Hardwareverifikation ; Pipeline-Verarbeitung ; Model checking ; Automatisches Beweisverfahren
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: In this thesis we describe the formal verification of a fully IEEE compliant floating point unit (FPU). The hardware is verified on the gate-level against a formalization of the IEEE standard. The verification is performed using the theorem proving system PVS. The FPU supports both single and double precision floating point numbers, normal and denormal numbers, all four IEEE rounding modes, and exceptions as required by the standard. Beside the verification of the combinatorial correctness of the FPUs we pipeline the FPUs to allow the integration into an out-of-order processor. We formally define the correctness criterion the pipelines must obey in order to work properly within the processor. We then describe a new methodology based on combining model checking and theorem proving for the verification of the pipelines.
Die vorliegende Arbeit behandelt die formale Verifikation einer vollständig IEEE konformen Floating Point Unit (FPU). Die Hardware wird auf Gatter-Ebene gegen eine Formalisierung des IEEE Standards verifiziert. Zur Verifikation wird das Beweis-System PVS benutzt. Die FPU unterstützt Fließkommazahlen mit einfacher und doppelter Genauigkeit, normale und denormale Zahlen, alle vier Rundungsmodi und alle Exception-Signale. Neben der Verifikation der kombinatorischen Schaltkreise werden die FPUs gepipelined, um sie in einen Out-of-order Prozessor zu integrieren. Die Korrektheits- Kriterien, die die gepipelineten FPUs befolgen müssen, um im Prozessor korrekt zu arbeiten, werden formal definiert. Es wird eine neue Methode zur Verifikation solcher Pipelines beschrieben. Die Methode beruht auf der Kombination von Model-Checking und Theorem-Proving.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-1915
hdl:20.500.11880/25760
http://dx.doi.org/10.22028/D291-25704
Erstgutachter: Wolfgang J. Paul
Tag der mündlichen Prüfung: 25-Okt-2002
SciDok-Publikation: 7-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 
ChristianJacobi_ProfDrWolfgangJPaul.pdf930,94 kBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.