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
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 SizeFormat 
ChristianJacobi_ProfDrWolfgangJPaul.pdf930,94 kBAdobe PDFView/Open

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