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.
(
geocities.com/de/christian_jacobi) (
geocities.com/de)