@InProceedings{bj01:vamp-fpu,
  title =	{Formal Verification of the {VAMP} Floating Point Unit},
  author =	{Christoph Berg and Christian Jacobi},
  series =	{LNCS},
  volume =	{2144},
  booktitle =	{CHARME 2001},
  pages =	{325--339},
  month =	sep,
  year =	{2001},
  publisher =	{Springer},
  pdf =		{2001/charme01-vamp-fpu.pdf},
  slides =	{2001/charme01-vamp-fpu-slides.ps.gz},
  springer =	{http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2144&spage=325},
  bibtex =	{2001/charme01-vamp-fpu.bib},
  abstract =	{We report on the formal verification of the floating point unit used
	in the VAMP processor.  The FPU is fully IEEE compliant, and supports
	denormals and exceptions in hardware. The supported operations are
	addition, subtraction, multiplication, division, comparison, and
	conversions. The hardware is verified on the gate level against a
	formal description of the IEEE standard by means of the theorem prover
	PVS.}
}