[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 #52 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Jacob Lifshay from comment #51)
> (In reply to Luke Kenneth Casson Leighton from comment #50)
> > >   Blocked on: https://github.com/YosysHQ/sby/pull/170
> 
> jix replied:
> https://github.com/YosysHQ/sby/pull/170#issuecomment-1160477086
> > <snip> I think the way to do this instead
> > would be extend `hierarchy -simcheck` to have a mode where it allows
> > blackboxes with an `smtlib2_module` attribute and then to use that mode
> > in sby's print_common_prep only when called for generating an smtlib2 output.
> 
> imho that's a pretty good idea -- I'll implement it soon.

I implemented it in https://github.com/YosysHQ/sby/pull/170 and
https://github.com/YosysHQ/yosys/pull/3391

veera: I completely rewrote the changes in #170, so if/when you get around to
adding it to dev-env-setup, you'll need to use the new commits, not the old
ones. it should work by using the 

I pushed the changes to the smtlib2-expr-support-on-0.13 yosys branch and to
the add-simcheck-option (wrong name, but keeping for consistency) branch in
SymbiYosys.git

I also updated the nmigen .gitlab-ci.yml, it's currently running

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