@Misc{berg:vamp-fpu-talk-2001,
  author =	{Christoph Berg},
  title =	{Verifikation der {VAMP}-{F}loating {P}oint {U}nit},
  booktitle =	{},
  year =	2001,
  month =	jul,
  day =		2,
  note =	{Graduiertenkolleg Leistungsgarantien für Rechnersysteme, Universität des Saarlandes},
  bibtex =	{2001/vamp.bib},
  slides =	{2001/vamp.ps.gz},
  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.},
}