[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 #20 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #19)
> i just increased the budget here, might have to do so again:

Thanks!

> 
> 1) just ran the unit tests, confirmed functional except for cvc4 is missing
>   if depending on cvc4 that will need adding to the dev-env-setup scripts
>   (symbiflow install one)
> 
>    is there a reason why cvc4 was picked instead of cvc5?

yes, cvc4 is supported by sby, cvc5 isn't yet afaict.

> 2) is this genuinely going to be independent? as in, no actual modifications
>    to nmigen itself needed? (apart from the addition to FHDLTestCase)
> 
>    if so, my feeling is that due to the build dependencies introduced
>    (cvc4, a maintenance-branch of yosys)

that's going into yosys master. nmigen master should be designed to work with
yosys master, not only yosys 0.13. the gitlab-ci stuff i'm adding runs tests
with both yosys master and 0.13.

the yosys 0.13 stuff is only because libre-soc doesn't want to upgrade for ls2,
not because later versions of yosys all don't work.

> it *may* be better to have this
>    as an entirely stand-alone repository

imho it should be in nmigen. the api may be changed to integrate more closely
with nmigen's AST -- e.g. SmtBitVec can be converted directly to a nmigen
Value, and the rtlil backend will insert the $smtlib2_expr instances, rather
than having the user have to do that manually via m.submodules.

e.g.

m.d.comb += Assert(bitvec.to_value() != 23)

rather than what is currently needed:

bitvec_submod = bitvec.to_signal()
m.submodules += bitvec_submod
m.d.comb += Assert(bitvec_submod.o_sig != 23)

and, no, having a SmtBitVec be a Value isn't a good idea since the API is based
on the smtlib2 specification, not nmigen's Value API.

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