Pubs-floating-point-arithmetic
Floating Point Arithmetic
- ACL2 Support for Floating-Point
Computations, M. Kaufmann and J S. Moore,
The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part
I (Cavalcanti, A. and Baxter, J., Eds), Springer Nature Switzerland,
Cham, pp 251-207, DOI https://doi.org/10.1007/978-3-031-66676-6_13, 2024.
-
A Case Study in Formal Verification of Register-Transfer Logic with ACL2:
The Floating Point Adder of the AMD Athlon Processor, David Russinoff.
Invited paper in Warren A. Hunt Jr. and
Steven D. Johnson (eds.), Proceedings of the Third International Conference on Formal Methods
in Computer-Aided Design (FMCAD 2000), Springer-Verlag LNCS 1954, 2000.
This is a proof of IEEE-compliance, as an application of a mechanical proof system for RTL designs based
on ACL2.
- RTL Verification: A Floating-Point Multiplier, David M. Russinoff and
Arthur Flatau, Chapter 13 of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/multiplier/ in the community-books.)
This article describes a mechanical proof system for designs
represented in the RTL language of Advanced Micro Devices. The system
consists of a translator to ACL2 and a methodology for verifying properties
of the resulting programs using the ACL2 prover. The correctness of a simple
floating-point multiplier is proved. The ACL2 scripts referenced here
provide the full details of the results described in the article along with
solutions to all the exercises in the article.
- A Mechanically Checked Proof of the
Correctness of the Kernel of the AMD5K86 Floating-Point Division
Algorithm, J Moore, Tom Lynch, and Matt Kaufmann, IEEE Transactions on
Computers, 47(9), pp. 913-926, Sep., 1998. This is the original (
March, 1996) version of our paper describing the mathematical details of the
proof that the FDIV microcode on the AMD K5 correctly implements IEEE
floating point division. The paper underwent extensive revision during the
reviewing process.
- A
Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level
Specification of the AMD K7 Floating Point Multiplication, Division and
Square Root Instructions, David Russinoff, Advanced Micro Devices, Inc.,
January, 1998. This paper is a tour de force in mechanical
verification. The paper describes a mechanically verified proof of
correctness of the floating-point multiplication, division, and square root
instructions of The AMD K7 microprocessor. The instructions, which are based
on Goldschmidt's Algorithm, are implemented in hardware and represented by
register-transfer level specifications, the primitives of which are logical
operations on bit vectors. On the other hand, the statements of correctness,
derived from IEEE Standard 754, are arithmetic in nature and considerably
more abstract. Therefore, the paper develops a theory of bit vectors and
their role in floating-point representations and rounding, extending previous
work (below) in connection with the K5 FPU. The paper then presents the
hardware model and a rigorous and detailed proof of its correctness. All of
the definitions, lemmas, and theorems have been formally encoded in the ACL2
logic, and every step in the proof has been mechanically checked with the
ACL2 prover.
- A Mechanically
Checked Proof of IEEE Compliance of the AMD K5 Floating-Point Square Root
Microcode, David Russinoff, Formal Methods in System Design
Special Issue on Arithmetic Circuits, 1997. The paper presents a rigorous
mathematical proof of the correctness of the FSQRT instruction of the AMD K5
microprocessor. The instruction is represented as a program in a formal
language that was designed for this purpose, based on the K5 microcode and
the architecture of its FPU. The paper proves a statement of its correctness
that corresponds directly with the IEEE standard. It also derives an
equivalent formulation, expressed in terms of rational arithmetic, which has
been encoded as a formula in the ACL2 logic and mechanically verified with
the ACL2 prover. Finally, the paper describes a microcode modification that
was implemented as a result of this analysis in order to ensure the
correctness of the instruction.
