Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

11

CHARME
2001
Springer

favoriteEmaildiscussreport

92views Hardware» more CHARME 2001»

Formal Verification of the VAMP Floating Point Unit

13 years 8 months ago

Formal Verification of the VAMP Floating Point Unit

Download www.df7cb.de

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.

Christoph Berg, Christian Jacobi 0002

Real-time Traffic

CHARME 2001 | Floating Point Unit | Formal Verification | Hardware | Theorem Prover Pvs |

claim paper

Related Content

» Formal Verification of Floating Point Trigonometric Functions

» A MachineChecked Theory of Floating Point Arithmetic

» Formal Verification of FloatingPoint Programs

» MultiProver Verification of FloatingPoint Programs

» Formal Verification of IA64 Division Algorithms

» Formal Verification of a Superscalar Execution Unit

» Construction of concrete verification models from C

» Combining ACL2 and an automated verification tool to verify a multiplier

» Leading Zero Anticipation and DetectionA Comparison of Methods

Post Info
More Details (n/a)

Added	23 Aug 2010
Updated	23 Aug 2010
Type	Conference
Year	2001
Where	CHARME
Authors	Christoph Berg, Christian Jacobi 0002

Comments (0)