Formal verification of the VAMP floating point unit

DOI10.1007/S10703-005-1613-YzbMATH Open1086.68518OpenAlexW2157753532MaRDI QIDQ816201FDOQ816201

Authors: Christian Jacobi, Christoph Berg 

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

Recommendations

• scientific article; zbMATH DE number 1852167
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Formal verification of floating-point hardware design. A mathematical approach
• scientific article; zbMATH DE number 1949625
• Verified compilation of floating-point computations

zbMATH Keywords

theorem provingformal verificationPVSfloating point unitIEEE standard 754

Mathematics Subject Classification ID

Computer system organization (68M99)

Cites Work

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

Cited In (13)

• Title not available (Why is that?)
• A formally verified floating-point implementation of the compact position reporting algorithm
• Finding normal binary floating-point factors efficiently
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Title not available (Why is that?)
• FM 2005: Formal Methods
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
• Title not available (Why is that?)
• Correct Hardware Design and Verification Methods
• Title not available (Why is that?)

Uses Software

• ACL2
• PVS
• HOL Light

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q816201)