Formal Verification of the VAMP Floating Point Unit

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.

• Type: Conference
• Year: 2001
• Where: CHARME
• Authors: Christoph Berg, Christian Jacobi 0002
• Keywords: CHARME 2001, Floating Point Unit, Formal Verification, Hardware, Theorem Prover Pvs