[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 #6 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Jacob Lifshay from comment #4)
> 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"

if we just rehashed the implementation verbatim in the formal correctness
proof, then we'd be lying if we said the formal proof was any better than the
original unknown-correctness nmigen code, we'd only be checking that the
original code gives the same answers when run in a formal proof, not that those
answers are actually correct.
> 
> 2) reimplement (effectively) the algorithms in "simple" (obvious)
>     reviewable fashion and use straight "equals"

that requires the fp code we have to implement at least one of the rounding
modes correctly, otherwise it'll give different results than the formal proof's
correct rounding, causing the equality to fail. this also kinda requires real
numbers to compute the correctly rounded result to compare against.
> 
> 3) compute error-bounds (erf, error-function) and check results

that generally requires real numbers of some sort...and no, the error function
isn't what you'd want here...that has to do with statistics of normal
distributions, not bounding the mathematical error in fp operations (unless
that fp operation is an implementation of the erf function).
> 
> 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.