Please use this identifier to cite or link to this item:
doi:10.22028/D291-25704
Title: | Formal verification of a fully IEEE compliant floating point unit |
Author(s): | Jacobi, Christian |
Language: | English |
Year of Publication: | 2002 |
SWD key words: | Mikroprozessor ; Gleitkommarechnung ; Hardwareverifikation ; Pipeline-Verarbeitung ; Model checking ; Automatisches Beweisverfahren |
DDC notations: | 004 Computer science, internet |
Publikation type: | Dissertation |
Abstract: | 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 to this record: | urn:nbn:de:bsz:291-scidok-1915 hdl:20.500.11880/25760 http://dx.doi.org/10.22028/D291-25704 |
Advisor: | Wolfgang J. Paul |
Date of oral examination: | 25-Oct-2002 |
Date of registration: | 7-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 | |
---|---|---|---|---|
ChristianJacobi_ProfDrWolfgangJPaul.pdf | 930,94 kB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.