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

basically yes.

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

yeah absolutely great. if you're happy to create a gitlab account then
pull-requests can be submitted there.  for yosys please base it off of
0.13, i'll create a repo on git.libre-soc.org shortly

$ yosys --version
Yosys 0.13 (git sha1 8b1eafc3a, clang 9.0.1-12 -fPIC -Os)

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