Formal Verification of the VAMP Floating Point Unit

Christoph Berg
Christian Jacobi

Open link

Publication date

January 2001

DOI

10.1007/3-540-44798-9_26

Publisher

Springer-Verlag

ISSN

0302-9743

Citation count (estimate)

Abstract

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.

Extracted data

We use cookies to provide a better user experience.

Data Protection

Formal Verification of the VAMP Floating Point Unit

Abstract

Extracted data

Formal Verification of the VAMP Floating Point Unit

Abstract

Extracted data

Related items

Related items