[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 #51 from Jacob Lifshay <programmerjake at gmail.com> ---
(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
> I would prefer if sby automatically does the right thing here instead of
> adding an option that removes the simcheck completely. Skipping the
> simcheck would allow using blackboxes to pass incomplete smtlib2 files
> to smtbmc and then on to the solvers. 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.

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