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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #3 from Jacob Lifshay <programmerjake at gmail.com> ---
I wrote most of the code needed to get nmigen to be able to generate smtlib2
expressions -- all of Bool, Int, Real, RoundingMode, and BitVec are
implemented, I'm still working on FloatingPoint. I also need to write tests.

It's designed so you can convert Bool and BitVec values to a nmigen
elaboratable with an output signal attribute...that is much easier, requiring
no modifications to the rest of nmigen, than trying to get the rtlil backend to
generate the instance as a submodule when needed, which would be hugely
invasive.

I pushed it to the smtlib2-expr-support branch:
https://git.libre-soc.org/?p=nmigen.git;a=commitdiff;h=8429519f5e64a81c5ff439be3db0238c5899906d

Once I have it working, I'll open a PR upstream on gitlab.com.

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