Campus Event Calendar
Event Entry
New for: D3
What and Who
Verifikation der VAMP-Floating Point Unit
Christoph Berg
Seminar des Graduiertenkollegs
AG 1, AG 2, AG 3, AG 4
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 2 July 2001
16:00
-- Not specified --
36 - Informatik
306
Saarbrücken
Abstract
Hardware zur Behandlung von Gleitkommazahlen ist sehr komplex und
Korrektheit kann nicht alleine durch Tests sichergestellt werden.
Mittels formaler Verifikation wird die Übereinstimmung der Hardware mit
einer Spezifikation bewiesen.
Ich stelle das VAMP-Projekt vor, in dem am Lehrstuhl Paul der
RISC-Prozessor VAMP (Verified Architecture MicroProcessor) verifiziert
wird. Die Floating Point Unit (FPU) des VAMP unterstützt die Operationen
Addition/Subtraktion, Multiplikation/Division, Vergleiche
und Konversionen. Denormale Zahlen und Exceptions werden in Hardware
behandelt.
Die Schaltkreise der VAMP-FPU werden auf Gatterebene (d.h. mit
UND/ODER/NICHT-Gattern) in der Sprache des Theorembeweisers PVS
implementiert. Gleichzeitig wird der IEEE Standard 754, in dem
Gleitkomma-Arithmetik definiert wird, in PVS formalisiert. Die
Spezifikation der FPU sagt nun aus, daß die von der FPU ausgeführten
Rechnungen dem IEEE-Standard entsprechen. Die Übereinstimmung der
Implementierung mit der Spezifikation wird mittels PVS bewiesen.
Der Vortrag gibt einen Überblick über das Verifikations-Projekt und
skizziert den Beweisansatz. Als Ausblick wird auf die Implementierung
des VAMP auf einem FPGA eingegangen
Ich stelle das VAMP-Projekt vor, in dem am Lehrstuhl Paul der
RISC-Prozessor VAMP (Verified Architecture MicroProcessor) verifiziert
wird. Die Floating Point Unit (FPU) des VAMP unterstützt die Operationen
Addition/Subtraktion, Multiplikation/Division, Vergleiche
und Konversionen. Denormale Zahlen und Exceptions werden in Hardware
behandelt.
Die Schaltkreise der VAMP-FPU werden auf Gatterebene (d.h. mit
UND/ODER/NICHT-Gattern) in der Sprache des Theorembeweisers PVS
implementiert. Gleichzeitig wird der IEEE Standard 754, in dem
Gleitkomma-Arithmetik definiert wird, in PVS formalisiert. Die
Spezifikation der FPU sagt nun aus, daß die von der FPU ausgeführten
Rechnungen dem IEEE-Standard entsprechen. Die Übereinstimmung der
Implementierung mit der Spezifikation wird mittels PVS bewiesen.
Der Vortrag gibt einen Überblick über das Verifikations-Projekt und
skizziert den Beweisansatz. Als Ausblick wird auf die Implementierung
des VAMP auf einem FPGA eingegangen
Contact
--email hidden
passcode not visible
logged in users only