In this thesis we describe the formal verification of a fully IEEE
compliant floating point unit (FPU). The hardware is verified on the
gate-level against a formalization of the IEEE standard. The
verification is performed using the theorem proving system PVS. The
FPU supports both single and double precision floating point numbers,
normal and denormal numbers, all four IEEE rounding modes, and
exceptions as required by the standard.
Beside the verification of the combinatorial correctness of the FPUs
we pipeline the FPUs to allow the integration into an out-of-order
processor. We formally define the correctness criterion the pipelines
must obey in order to work properly within the processor. We then
describe a new methodology based on combining model checking and
theorem proving for the verification of the pipelines.
(
geocities.com/de/christian_jacobi) (
geocities.com/de)