A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor

DOI10.1112/S1461157000000176zbMath0910.68008OpenAlexW2099571283MaRDI QIDQ4230664

David M. Russinoff

Publication date: 8 February 1999

Published in: LMS Journal of Computation and Mathematics (Search for Journal in Brave)

Full work available at URL: http://www.lms.ac.uk/jcm/1/

zbMATH Keywords

formal hardware verification

Mathematics Subject Classification ID

Computing methodologies and applications (68U99) Mathematical problems of computer architecture (68M07) Computer aspects of numerical algorithms (65Y99)

Related Items (14)

Ordinal arithmetic: Algorithms and mechanization ⋮ A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures ⋮ Efficient and accurate computation of upper bounds of approximation errors ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ A parametric error analysis of Goldschmidt's division algorithm ⋮ Floating-point arithmetic in the Coq system ⋮ Hammering Floating-Point Arithmetic ⋮ Integrating external deduction tools with ACL2 ⋮ Hardware-Dependent Proofs of Numerical Programs ⋮ Formal Verification for High-Assurance Behavioral Synthesis ⋮ Verified compilation of floating-point computations ⋮ Formal verification of the VAMP floating point unit ⋮ Choosing starting values for certain Newton-Raphson iterations

Uses Software

• LISP
• NQTHM
• Unnamed Item

Cites Work

• A verification system for concurrent programs based on the Boyer-Moore prover
• Unnamed Item

This page was built for publication: A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor