@InProceedings{jb05-vamp-fmsd05,
  author =	{Christian Jacobi and Christoph Berg},
  title =	{Formal Verification of the {VAMP} Floating Point Unit},
  booktitle =	{Formal Methods in System Design},
  pages =	{227--266},
  year =	{2005},
  month =	may,
  publisher =	{Springer},
  pdf =		{2005/jb05-vamp-fmsd.pdf},
  bibtex =	{2005/jb05-vamp-fmsd.bib},
  springer =	{http://www.springerlink.com/openurl.asp?genre=article&issn=0925-9856&volume=26&issue=3&spage=227},
  abstract =	{
  We report on the formal verification of the floating point unit used in the
  VAMP processor. The dual-precision FPU is IEEE compliant and supports
  denormals and exceptions in hardware. The supported operations are addition,
  subtraction, multiplication, division, comparison, and conversions.

  We have formalized the IEEE standard 754. The formalization is supplemented
  by a rich theory of rounding, which includes notations and theorems
  facilitating the verification of the actual hardware. The theory of rounding
  enables the separation of the hardware into smaller modules which can be
  verified individually. Each module is verified on the gate level against a
  formal specification. The combination of these formal specifications,
  together with the theorems from the theory of rounding, yield the overall
  correctness of the FPU, i.e., theorems stating that the gate-level hardware
  complies with the high-level formalization of the IEEE standard. The
  verification is done completely in the theorem prover PVS.

  We further report on the implementation and test of the verified FPU on a
  Xilinx FPGA.},
}

    Source: geocities.com/de/christian_jacobi/publications

               ( geocities.com/de/christian_jacobi)                   ( geocities.com/de)