We report on the formal verification of a theory of IEEE rounding in
the theorem prover PVS. The theory consists of a formalization of the
IEEE standard, and notations and theorems facilitating the
verification of floating point hardware. In particular, the concepts
of $\alpha$-equivalence and round decomposition are formalized,
allowing for a subdivision of floating point units into smaller
building blocks, which then can be verified separately. The theory has
been successfully applied to the verification of a fully IEEE
compliant floating point unit.
(
geocities.com/de/christian_jacobi) (
geocities.com/de)