[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 #21 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #17)
> (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

I specifically chose fmul because it's slower...the idea is that if fmul is
feasible, nearly everything we'd want to implement will be feasible.

> > 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.

ok, though once we have the yosys parts working (I expect the only hard part to
be modifying the smtlib2 backend), i expect the nmigen support to be very quick
and easy -- around as fast as I can type.

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