[Libre-soc-bugs] [Bug 196] Formal correctness proof needed for the IEEE754 FPU

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=196

Luke Kenneth Casson Leighton <lkcl at lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |programmerjake at gmail.com

--- Comment #2 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
https://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf

some interesting leads and papers, it looks like there
have been quite a few Formal Correctness Proof attempts
on IEEE754 FP already.

which if true would make this more a task of applying
those rather than attempting to create a new one from
scratch.

that approach is IMPORTANT because those pre-existing
Proofs would be a "known-good".

attempting to reinvent the wheel unnecessarily actually
introduces the serious risk of not having provenance
behind the newly-invented Proof.

-- 
You are receiving this mail because:
You are on the CC list for the bug.