[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 #14 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Jacob Lifshay from comment #10)
> (In reply to Luke Kenneth Casson Leighton from comment #7)
> > 
> > yeah even if it existed we could in no way rely on FP number
> > representation, it would be machine-dependent and there is
> > just no way it could be trusted.  even if soft-implemented
> > (j hauser softfloat) that's still dicey.
> 
> smtlib2's fp types are machine independent.

Note smtlib2 is a specification for a format that sat solvers can read their
inputs in.

elaborating more, smtlib2's fp support is specifically designed to be machine
independent, for example, there is no way to determine which NaN a particular
fp op returns, smtlib2 treats all NaNs identically. all you can do is see you
got a NaN, not which NaN:
Quoting the spec:
https://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml
> There is no function for converting from (_ FloatingPoint eb sb) to the
> corresponding IEEE 754-2008 binary format, as a bit vector (_ BitVec m) with 
> m = eb + sb, because (_ NaN eb sb) has multiple, well-defined representations.
> Instead, an encoding of the kind below is recommended, where f is a term
> of sort (_ FloatingPoint eb sb):
> 
>  (declare-fun b () (_ BitVec m))
>  (assert (= ((_ to_fp eb sb) b) f))

also, smtlib2 supports fp formats with arbitrary user-specified exponent and
mantissa sizes, so it can also easily be used to test bf16 ops.

If you're worried the fp implementation they use might be buggy, the solution
is utterly simple -- just run your tests with more than one sat solver, they
shouldn't all have the exact same bugs.

therefore, I think smtlib2's fp can be relied upon to be correct.

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