[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

--- Comment #4 from Jacob Lifshay <programmerjake at gmail.com> ---
from email with lkcl -- in response to concern about yosys not supporting real
numbers (i corrected some spelling errors):
basically there are a number of
potential approaches:

1) cheat.  proofs are done on submodules in a verbatim fashion.
    "this module intends to do X therefore test for X with very little
     thought as to the bigger picture"

2) reimplement (effectively) the algorithms in "simple" (obvious)
    reviewable fashion and use straight "equals"

3) compute error-bounds (erf, error-function) and check results

4) find someone else's papers or formal verification technique
    e.g. https://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf

this should go on mailing list.  my guess is (3) will have lots
of papers online about error-bounds of IEEE754 FP.

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