Formal verification of the VAMP floating point unit

DOI10.1007/s10703-005-1613-yzbMath1086.68518OpenAlexW2157753532MaRDI QIDQ816201

Christoph Berg, Christian Jacobi

Publication date: 20 February 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-005-1613-y

zbMATH Keywords

theorem provingformal verificationPVSfloating point unitIEEE standard 754

Mathematics Subject Classification ID

Computer system organization (68M99)

Related Items (1)

Finding normal binary floating-point factors efficiently

Uses Software

• ACL2
• PVS
• HOL Light

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A proof of the nonrestoring division algorithm and its implementation on an ALU
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• On the design of IEEE compliant floating point units
• Correct Hardware Design and Verification Methods

This page was built for publication: Formal verification of the VAMP floating point unit