[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 #11 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #9)
> (In reply to Jacob Lifshay from comment #6)
> 
> > > 
> > > 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 problem is that the mere act of generating an answer encoded as a fp number
*is rounding* (even if not following any defined rounding mode).
> 
> the proof would also not have rounding and would also have it added later.

unless you can make the proof round in exactly the same way as the algorithm
your testing against, the proof will always have assertion failures where the
rounding has a mismatch.
> 
> 
> > > 
> > > 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.

that's done using arbitrary-precision rational numbers and/or bigints...another
set of things smtlib2 supports that nmigen/yosys doesn't.

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