Formal Verification of the VAMP Floating Point Unit

Christoph Berg and Christian Jacobi

Saarland University
Computer Science Department
D-66123 Saarbruecken, Germany
Fax: +49/681/302-4290
{cb,cj}@cs.uni-sb.de 

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. 

LNCS 2144, p. 325 ff.