[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 #9 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #6)

> 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.

the idea was even worse than that :)  just do a real basic proof of
"the normalisation class" and so on. it was not a serious suggestion
but one that is easy to do and perhaps might work if they are chained
together then tested against other implementations.

> > 
> > 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.

we discussed the flexible solution here to not implement rounding yet and
come back to it later during a second phase.

the proof would also not have rounding and would also have it added later.


> > 
> > 3) compute error-bounds (erf, error-function) and check results
> 
> that generally requires real numbers of some sort...

ah no.  i mean in digital form. express the expected difference in
digital form.  similar to that Goldberg iteration checking thing.

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