[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 #26 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #25)
> (In reply to Luke Kenneth Casson Leighton from comment #23)
> 
> > dumping values in case it returned sat:
> > ((a #x80000000)
> 
> minus zero
> 
> >  (b #xff800000)
> 
> times minus infinity
> 
> >  (p #x7f800002)
> 
> would be plus infinity if not for the 2

yup, p is a NaN. p is the output of smtlib2's fp.mul.

what isn't correct is the output of f32_mul_rne which is the fmul that I wrote
using bitvectors.

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