FYI: some references for formal models and verification of IEEE floating point

[rsnikhil]

This information may be of use/interest re. formalization of IEEE Floating Point in Sail.

A prominent contributor is John Harrison who used to be at Intel (and U.Cambridge before that) and I believe is now at Amazon Web Services: https://www.cl.cam.ac.uk/~jrh13/

Here is a list of publications/talks involving John Harrison:
https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=John+Harrison+HOL+IEEE+floating+point&btnG=

A few other references of interest:

Verilog Golden Model (VGM) library:
by Warren Ferguson and Flemming Andersen
This supposedly contains a Verilog Golden Model for IEEE Floating Point.
Available with an open-source license (BSD).

Paper: "CREST: Hardware Formal Verification with ANSI-C Reference Specifications"
by Andreas Tiemeyer, Tom Melham, Daniel Kroening and John O’Leary
August 2019
https://arxiv.org/pdf/1908.01324.pdf
Contains, as a case study, a formal verification of Softfloat vs. VGM

Paper: "Verifying a Synthesized Implementation of IEEE-754
Floating-Point Exponential Function using HOL"
by Behzad Akbarpour, Amr T. Abdel-Hamid, Sofiène Tahar and John Harrison

Tutorial: "HOL Light: A tutorial introduction"
by John Harrison
In Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996

Paper: "A Parameterized Floating-Point Formalizaton in HOL Light"
by Charles Jacobsen, Alexey Solovyev and Ganesh Gopalakrishnan (Univ. of Utah)

[PeterSewell]

There's also a bunch of stuff in Coq: https://proofassistants.stackexchange.com/questions/86/how-can-i-prove-facts-about-floating-point-calculations and the Arm approach of using real-number definitions of operations and converting into bits. Peter

…

On Mon, 15 Apr 2024 at 14:48, Rishiyur S. Nikhil ***@***.***> wrote: This information may be of use/interest re. formalization of IEEE Floating Point in Sail. A prominent contributor is John Harrison who used to be at Intel (and U.Cambridge before that) and I believe is now at Amazon Web Services: https://www.cl.cam.ac.uk/~jrh13/ Here is a list of publications/talks involving John Harrison: https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=John+Harrison+HOL+IEEE+floating+point&btnG= A few other references of interest: Verilog Golden Model (VGM) library: by Warren Ferguson and Flemming Andersen This supposedly contains a Verilog Golden Model for IEEE Floating Point. Available with an open-source license (BSD). Paper: "CREST: Hardware Formal Verification with ANSI-C Reference Specifications" by Andreas Tiemeyer, Tom Melham, Daniel Kroening and John O’Leary August 2019 https://arxiv.org/pdf/1908.01324.pdf Contains, as a case study, a formal verification of Softfloat vs. VGM Paper: "Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL" by Behzad Akbarpour, Amr T. Abdel-Hamid, Sofiène Tahar and John Harrison Tutorial: "HOL Light: A tutorial introduction" by John Harrison In Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996 Paper: "A Parameterized Floating-Point Formalizaton in HOL Light" by Charles Jacobsen, Alexey Solovyev and Ganesh Gopalakrishnan (Univ. of Utah) — Reply to this email directly, view it on GitHub <#451>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFMZZTLKNUOBB6ZUOAUALDY5PLAZAVCNFSM6AAAAABGHM4EBGVHI2DSMVQWIX3LMV43ERDJONRXK43TNFXW4OZWGUYDSOBUGI> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>