[Libre-soc-bugs] [Bug 835] add support for smtlib2 floating-point to yosys and nmigen

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Thu Jun 16 09:35:49 BST 2022


https://bugs.libre-soc.org/show_bug.cgi?id=835

--- Comment #48 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #47)
> if you think you can complete the ENTIRE Formal Correctness Proofs in nmigen
> in UNDER TWO MONTHS, *and get the RFP in*, then "waiting" is "perfectly fine"

I never expected to be able to complete all the formal proofs, but I think I
can definitely get at least some working...they likely won't be perfect since
we're missing support for ieee754 exception bits.

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


More information about the libre-soc-bugs mailing list