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.