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

>     It's probably correct, z3 ran longer than I bothered to wait, it usually
> stops relatively quickly if there's an error in the logic.

yes, mul is awful.  fpadd would have been much faster

(In reply to Jacob Lifshay from comment #14)

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

oo that's a really good sign.

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

ah. and FP8 which someone from the IBM India Education Course wants
to investigate.

(In reply to Jacob Lifshay from comment #15)

> therefore, I think the best route is to instead add a new built-in cell
> type, where all inputs/outputs are still bitvectors/bools but internally it
> can do real/fp ops. it would have a parameter with the expression to
> evaluate (probably as a string). all of yosys would treat it as a black box,
> except for the smtlib2 backend which would put the expression in the
> appropriate place in the generated output.

nice. elegant hack. means we need a yosys git repo but that's ok.

> nmigen could be extended with helper classes/functions to make it easier to
> generate those expression cells, though that's not technically necessary.

well anything that makes life easier is good: an IT sysadmin rule i heard,
if you do something more than even just once, script it :)

it's Friday and i have a meeting with the IBM India team today, i will
see what the Professor thinks. he has students who could help.

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