[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 #33 from Jacob Lifshay <programmerjake at gmail.com> ---
so, i think smtlib2 fp will be useful, though probably won't be able to prove
everything, so there we'll probably have to rely on fp16 being proven correct
and fp32/fp64 assumed to be correct because we ran lots of tests and the same
code is known to work for fp16.

I'd like to start working on adding support for it to yosys and nmigen, does
that sound good? (should be a separate bug)

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