helpful insights from jix on yosys irc:

<lkcl> Float16 (and Float32) isn't recognised by yosys. that's what we have to "pass through" in some easy form that doesn't involve a massive amount of work
<jix> why not use blackbox modules for the fp primitives you need that use normal signals (i.e. BitVecs) for their ports and supply your own smt2 definition for them that internally can convert to floating point types?
<jix> that would only need small changes to sby to allow adding user smt2 statements but no changes to yosys or smtbmc
<jix> lkcl: also fwiw bitwuzla using kissat as SAT backend solves fp16mul_test.smt2 a lot faster than z3 (after inlining f16_to_fp and changing all (define-const foo ...) to (define-fun foo () ...) to make bitwuzla's parser happy)
<jix> kissat upstream doesn't support incremental solving yet, but I do have experimental patches for kissat to add that (and a patch to bitwuzla to enable that)
<jix> but incremental solving isn't needed for this smt2 file and for smtbmc it's optional (there's a -noincr option)
<jix> and bitwuzla with cadical (default SAT backend) is probably still faster than z3
<jix> not convinced that bitwuzla can crack the 32-bit float version, though, but I'm curious so I'll let it run overnight

I added all of what I think we'll need in yosys for the smtlib2 passthrough cell:
https://git.libre-soc.org/?p=yosys.git;a=shortlog;h=refs/heads/smtlib2-expr-support

I opened a draft PR here:
https://github.com/YosysHQ/yosys/pull/3319

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.

that entire repo is out of date and should not be used.
i simply haven't had time to extract work in it yet.
can you please redo on gitlab bearing in mind under NO
circumstances do a force-push and that the entire commit
history hashes are completely different.

(In reply to Luke Kenneth Casson Leighton from comment #4)
> that entire repo is out of date and should not be used.
> i simply haven't had time to extract work in it yet.
> can you please redo on gitlab bearing in mind under NO
> circumstances do a force-push and that the entire commit
> history hashes are completely different.

well, had you checked the history on the git branch I pushed, you would have seen it's actually based on latest master from gitlab

https://git.libre-soc.org/?p=nmigen.git;a=shortlog;h=refs/heads/smtlib2-expr-support

I created a repo on gitlab and am pushing my work there in addition to git.libre-soc.org:
https://gitlab.com/programmerjake/nmigen/-/commits/smtlib2-expr-support

I discovered that nmigen's tests were broken (because lkcl didn't run the tests when he added *_prst pins to the pin_layout function), and submitted a PR to fix that:
https://gitlab.com/nmigen/nmigen/-/merge_requests/6

I added smtlib2 floating-point support to nmigen, but didn't add tests yet.

I implemented tests for all supported smtlib2 sorts (smtlib2's name for types) and for SmtBool's functions.

It works correctly in formal proofs! (though I had to fix yosys-smtbmc's overly simplistic parser, added to the draft yosys PR)

I created a draft PR for this on nmigen's repo:
https://gitlab.com/nmigen/nmigen/-/merge_requests/7

(In reply to Jacob Lifshay from comment #5)
> (In reply to Luke Kenneth Casson Leighton from comment #4)
> > that entire repo is out of date and should not be used.
> > i simply haven't had time to extract work in it yet.
> > can you please redo on gitlab bearing in mind under NO
> > circumstances do a force-push and that the entire commit
> > history hashes are completely different.
> 
> well, had you checked the history on the git branch I pushed, you would have
> seen it's actually based on latest master from gitlab

that's *exactly* what i did not want to happen and if you'd
asked i would have said NO

there is still an extremely important branch that has NOT been forward-ported
because i haven't had time.

i'm locking down that repository and removing your commit rights.

you MUST NOT use force-push without consulting me

(In reply to Luke Kenneth Casson Leighton from comment #8)
> you MUST NOT use force-push without consulting me

I did *not* force push, it's a completely new branch

(In reply to Jacob Lifshay from comment #9)
> (In reply to Luke Kenneth Casson Leighton from comment #8)
> > you MUST NOT use force-push without consulting me
> 
> I did *not* force push, it's a completely new branch

sorry, i jumped to conclusions, i'm dehydrated and didn't sleep well.
once i've calmed down and had time to think i'll be able to evaluate
properly.

Added smtlib2 subexpression interning to avoid exponential blowup for things like:
a = SmtBitVec.make(sig)
for i in range(100):
    # would create 2 ** 100 subexpressions without interning
    a *= a

https://gitlab.com/nmigen/nmigen/-/merge_requests/7/diffs?commit_id=4022161b8ad467d44c65c76b3a8faf37a791144e

Found an issue with nmigen's // operator in formal proofs (it maps to yosys's $divfloor operator):
https://github.com/YosysHQ/yosys/issues/3330
so I had to use a workaround in the tests.

I'm realizing that this is getting a bit (but not a lot) bigger than expected...
1340 lines of new tests
(all of SmtBool, nearly all of SmtReal, no other smtlib2 types yet)

2618 lines in nmigen/hdl/smtlib2.py (completed afaict)

(In reply to Jacob Lifshay from comment #11)

> I'm realizing that this is getting a bit (but not a lot) bigger than
> expected...

not a problem just increase the budget accordingly

I made progress on adding all the tests for the nmigen integration.

I also submitted a PR adding $divfloor support to yosys's write_smt2 (which was missing):
https://github.com/YosysHQ/yosys/pull/3335

I finished adding tests and marked both the nmigen and yosys PRs as ready.

There ended up being 5.8kloc of tests and 2.6kloc of nmigen wrapper classes.

The tests have 100% coverage of the new source file.

I ran the tests using (in nmigen's root dir):
pytest -n auto --cov-report=xml:cov.xml --cov
coverage report --fail-under=100 --include='*/*smtlib2.py' -m

Last few lines of output:
============================= 869 passed in 12.99s =============================
Name                    Stmts   Miss Branch BrPart  Cover   Missing
-------------------------------------------------------------------
nmigen/hdl/smtlib2.py    1787      0    414      0   100%

(In reply to Jacob Lifshay from comment #13)
> I made progress on adding all the tests for the nmigen integration.
> 
> I also submitted a PR adding $divfloor support to yosys's write_smt2 (which
> was missing):
> https://github.com/YosysHQ/yosys/pull/3335

https://git.libre-soc.org/?p=yosys.git;a=log;h=refs/heads/smtlib2-expr-support

that's based off of the master branch.  we cannot use it.
i explained why in an earlier conversation.

https://git.libre-soc.org/?p=dev-env-setup.git;a=blob;f=hdl-tools-yosys;h=86d1a26f1598c65f0941c9d2ce6465cb815eb377;hb=HEAD#l35

yosys-0.13 and no other version has to be used.

From https://gitlab.com/nmigen/nmigen/-/merge_requests/7#note_960517715

> I cherry-picked the commits onto a branch based on yosys-0.13, I also added the
> commits for a ecp5 test fix and the new write_jny pass that sby needs, since
> both of those are needed for tests to pass.
> 
> https://git.libre-soc.org/?p=yosys.git;a=shortlog;h=refs/heads/smtlib2-expr-support-on-0.13
> or
> https://github.com/programmerjake/yosys/tree/smtlib2-expr-support-on-0.13

(In reply to Jacob Lifshay from comment #16)
> From https://gitlab.com/nmigen/nmigen/-/merge_requests/7#note_960517715
> 
> > I cherry-picked the commits onto a branch based on yosys-0.13, 

brilliant.  i'll need to update devscripts to pull from that.

(In reply to Luke Kenneth Casson Leighton from comment #17)
> (In reply to Jacob Lifshay from comment #16)
> > From https://gitlab.com/nmigen/nmigen/-/merge_requests/7#note_960517715
> > 
> > > I cherry-picked the commits onto a branch based on yosys-0.13, 
> 
> brilliant.  i'll need to update devscripts to pull from that.

imho we should instead create a new branch named libre-soc-0.13.x or something so it can include all yosys patches we need in case we need more in the future. those additional future patches shouldn't be on the branch i created as the naming implies it only has patches needed for $smtlib2_expr support.

i just increased the budget here, might have to do so again:

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?

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) it *may* be better to have this
   as an entirely stand-alone repository

(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.

(In reply to Jacob Lifshay from comment #20)

> the yosys 0.13 stuff is only because libre-soc doesn't want to upgrade for
> ls2, 

that's not correct: i have mentioned this already - it's down to instability
in yosys due to API changes. *nobody* can get yosys-ghdl-plugin working
and yosys-ghdl-plugin is needed for compiling microwatt.  this has absolutely
nothing to do with ls2, and everything to do with yosys changing APIs in a
way that makes them completely incompatible with critical plugins on which
the wider community critically relies.  in our case that's critical day-to-day
testing and development for the *entire* libre-soc codebase i.e. *all* SoCs
*all* versions past present and future because microwatt HDL-module-level
compatibility is absolute and fundamental to saving astounding amounts of
time and resources.

ghdl then *also* changed its internal data structures which made the situation
even more complex.

several days of searching and compiling across *three* separate repositories
eventually found the cross-over point between ghdl, yosys, and yosys-ghdl-plugin
that would actually work.

more later. summary: integration justification in nmigen makes sense.

(In reply to Luke Kenneth Casson Leighton from comment #21)
> (In reply to Jacob Lifshay from comment #20)
> 
> > the yosys 0.13 stuff is only because libre-soc doesn't want to upgrade for
> > ls2, 
> 
> that's not correct:
...
> several days of searching and compiling across *three* separate repositories
> eventually found the cross-over point between ghdl, yosys, and
> yosys-ghdl-plugin
> that would actually work.

afaict ghdl-yosys-plugin currently works on yosys master, last i checked (few days ago) i saw it in https://github.com/YosysHQ/oss-cad-suite-build nightly builds. (i'm assuming since it builds in CI it probably works, i haven't tested it tho)

see also: https://github.com/YosysHQ/oss-cad-suite-build/issues/14#issuecomment-945413116

> 
> more later. summary: integration justification in nmigen makes sense.

:)

(In reply to Jacob Lifshay from comment #22)

> afaict ghdl-yosys-plugin currently works on yosys master, last i checked
> (few days ago) i saw it in https://github.com/YosysHQ/oss-cad-suite-build
> nightly builds. (i'm assuming since it builds in CI it probably works, i
> haven't tested it tho)

got time to check it and also update all our documentation and the devscripts?
after running for four years now we're now into maintenance stability and
any tool upgrades have to be scheduled and planned well in advance.

(In reply to Luke Kenneth Casson Leighton from comment #23)
> (In reply to Jacob Lifshay from comment #22)
> 
> > afaict ghdl-yosys-plugin currently works on yosys master, last i checked
> > (few days ago) i saw it in https://github.com/YosysHQ/oss-cad-suite-build
> > nightly builds. (i'm assuming since it builds in CI it probably works, i
> > haven't tested it tho)
> 
> got time to check it and also update all our documentation and the
> devscripts?

idk if i'm the best one to work on that even if i do have time -- i haven't yet gotten around to getting coriolis2 working on my computer.

> after running for four years now we're now into maintenance stability and
> any tool upgrades have to be scheduled and planned well in advance.

yosys 0.13 isn't anywhere near that old, a few months at most:
https://github.com/YosysHQ/yosys/commit/8b1eafc3adc6ce6828cc827e518a4fa9425feb56.patch
Date: Tue, 11 Jan 2022 08:35:50 +0100
Subject: [PATCH] Release version 0.13

My point isn't as much that we should switch libre-soc to a later version of yosys (imho we should after ls2, but i'm fine if we put that off), but that nmigen shouldn't be designed to only work on yosys 0.13, it should be tested to work on yosys master too and we should use yosys master as the primary target that we aim for when maintaining nmigen and deciding if PRs are appropriate or not. having nmigen work on yosys 0.13 is secondary, but still important.

(In reply to Jacob Lifshay from comment #24)

> nmigen shouldn't be designed to only work on yosys 0.13, it should be tested
> to work on yosys master too

oh yehyehyeh of course, yes now i understand, absolutely agree.
the side-branch is effectively "our maintenance problem".

(In reply to Jacob Lifshay from comment #20)
> 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)

I changed the API so SmtBitVec and SmtBool are both ValueCastable, so you can do things like:

sort = SmtSortFloat32()
neg_zero = SmtFloatingPoint.neg_zero(sort=sort)
m.d.comb += Assert(fp1.same(neg_zero)) # same() returns a SmtBool, which is then cast to a Value by Assert.__init__

I also merged the CI additions into the smtlib2-expr-support branch and adjusted .gitlab-ci.yml to use our yosys 0.13 fork with the $smtlib2_expr support.

CI for yosys master fails because $smtlib2_expr isn't yet merged.

(In reply to Jacob Lifshay from comment #26)

> I changed the API so SmtBitVec and SmtBool are both ValueCastable,

sorry, can you please make that UserValue, i'm going to deprecate
ValueCastable because it breaks the chain of inheritance. this was
touted as a "feature" but it's a serious problem when adding the
up-casting we discussed a few months back.


> I also merged the CI additions into the smtlib2-expr-support branch and
> adjusted .gitlab-ci.yml to use our yosys 0.13 fork with the $smtlib2_expr
> support.

brilliant

> CI for yosys master fails because $smtlib2_expr isn't yet merged.

nice to have something keeping an eye on when that occurs

(In reply to Luke Kenneth Casson Leighton from comment #27)
> (In reply to Jacob Lifshay from comment #26)
> 
> > I changed the API so SmtBitVec and SmtBool are both ValueCastable,
> 
> sorry, can you please make that UserValue,

No, making it UserValue is a bad idea, it breaks the API, as I mentioned earlier:

(In reply to Jacob Lifshay from comment #20)
> 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.

UserValue and ValueCastable are both useful for different things...ValueCastable can be used for things that aren't a nmigen Value (such as SmtBitVec which has a different API than Value) but can be implicitly and/or explicitly converted to a Value, whereas UserValue is useful for things that are a Value but just have some extra features.

> i'm going to deprecate
> ValueCastable because it breaks the chain of inheritance.

Please don't, it's useful too. we can choose to have both UserValue and ValueCastable, they're useful for different things.

> this was
> touted as a "feature" but it's a serious problem when adding the
> up-casting we discussed a few months back.

that's because ValueCastable is the wrong tool for that job [1]. being the wrong tool for that job doesn't mean ValueCastable isn't useful for other jobs, such as SmtBitVec.

[1] assuming you want simd values to be nmigen Values -- i strongly disagree, but we can argue about that some other time.
> 
> 
> > I also merged the CI additions into the smtlib2-expr-support branch and
> > adjusted .gitlab-ci.yml to use our yosys 0.13 fork with the $smtlib2_expr
> > support.
> 
> brilliant
> 
> > CI for yosys master fails because $smtlib2_expr isn't yet merged.
> 
> nice to have something keeping an eye on when that occurs

I'm subscribed to the github PR(s), so can easily keep track of that. I'll most likely put a comment here and/or on the nmigen PR when the github PR is merged.

(In reply to Jacob Lifshay from comment #28)

> Please don't, it's useful too. we can choose to have both UserValue and
> ValueCastable, they're useful for different things.

unfortunately ValueCastable causes major showstopping problems.

> > this was
> > touted as a "feature" but it's a serious problem when adding the
> > up-casting we discussed a few months back.
> 
> that's because ValueCastable is the wrong tool for that job [1]. 

the problem is that ValueCastable fails "isinstance(Value)" as well as base
class chain inheritance detection. upcasting critically relies on detecting
the highest inherited class, and casting all objects specifically to that
type.

the fact that ValueCastable derivatives may be mixed with UserValue derivatives
makes it impossible to establish the up-casting chain and consequently ValueCastable has to go.

if you can come up with an upcasting function which guarantees that an arbitrary
list of objects that are of multiple inheritance types from *both* UserValue
*and* ValueCastable across *multiple third party libraries* then it can stay.
no, throwing an exception if a mix is detected is not acceptable because the
up-casting function must cope with arbitrary mixed third party objects.

> [1] assuming you want simd values to be nmigen Values -- i strongly
> disagree, but we can argue about that some other time.

sorry to have to say this, but tough. i know full well that you want a total duplication of the entire ast.py source code: i have already explained multiple times that that is a maintenance nightmare, is utterly unnecessary, and even worse than that it implies that there exists an API difference when there is absolutely none at all in any way shape or form. please re-read the RFC if you are not familiar with the logical reasoning.

> > 
> > 
> > > I also merged the CI additions into the smtlib2-expr-support branch and
> > > adjusted .gitlab-ci.yml to use our yosys 0.13 fork with the $smtlib2_expr
> > > support.
> > 
> > brilliant
> > 
> > > CI for yosys master fails because $smtlib2_expr isn't yet merged.
> > 
> > nice to have something keeping an eye on when that occurs
> 
> I'm subscribed to the github PR(s), so can easily keep track of that. I'll
> most likely put a comment here and/or on the nmigen PR when the github PR is
> merged.

(In reply to Luke Kenneth Casson Leighton from comment #29)

> duplication of the entire ast.py source code:

sorry, i meant dsl.py (containing Module)

(In reply to Luke Kenneth Casson Leighton from comment #29)
> (In reply to Jacob Lifshay from comment #28)
> > > this was
> > > touted as a "feature" but it's a serious problem when adding the
> > > up-casting we discussed a few months back.
> > 
> > that's because ValueCastable is the wrong tool for that job [1]. 
> 
> the problem is that ValueCastable fails "isinstance(Value)" as well as base
> class chain inheritance detection. upcasting critically relies on detecting
> the highest inherited class, and casting all objects specifically to that
> type.

There's a simple solution, which you're missing because you're still trying to cram ValueCastable into a Value-shaped hole where it doesn't fit -- a ValueCastable *isn't* a Value and doesn't need to behave like one: just call as_value() on all ValueCastable instances and do all the inheritance detection and highest inherited class stuff on the objects you get:

e.g.:
def Cat(*args):
    args_l = []
    for arg in flatten(args):
        if not isinstance(arg, Value):
            # converts ValueCastable, skipped for UserValue
            arg = Value.cast(arg)
        args_l.append(arg)
    # now calculate most-derived class based on args_l
    ...
> 
> the fact that ValueCastable derivatives may be mixed with UserValue
> derivatives
> makes it impossible to establish the up-casting chain and consequently
> ValueCastable has to go.
> 
> if you can come up with an upcasting function which guarantees that an
> arbitrary
> list of objects that are of multiple inheritance types from *both* UserValue
> *and* ValueCastable across *multiple third party libraries* then it can stay.

I did, see above.

> no, throwing an exception if a mix is detected is not acceptable because the
> up-casting function must cope with arbitrary mixed third party objects.
> 
> > [1] assuming you want simd values to be nmigen Values -- i strongly
> > disagree, but we can argue about that some other time.
> 
> sorry to have to say this, but tough. i know full well that you want a total
> duplication of the entire ast.py source code: i have already explained
> multiple times that that is a maintenance nightmare, is utterly unnecessary,
> and even worse than that it implies that there exists an API difference when
> there is absolutely none at all in any way shape or form. please re-read the
> RFC if you are not familiar with the logical reasoning.

we can argue about that some other time.

(In reply to Jacob Lifshay from comment #31)
 
> There's a simple solution, which you're missing because you're still trying
> to cram ValueCastable into a Value-shaped hole where it doesn't fit -- a
> ValueCastable *isn't* a Value

that you recommend this indicates that you do not understand the paradigm
of the abstraction concept, at all.  it also explains why you keep recommending
to duplicate the entire dsl.py source code.

can i leave it with you to work out, over the next few weeks/months, why
that is? don't think about it too much, but just consider over time,
"why would luke say that that idea isn't going to work? why is it
 critically and fundamentally important that all objects be upcast to
 the highest-identified Cast function, no exceptions"?

(In reply to Luke Kenneth Casson Leighton from comment #32)
> (In reply to Jacob Lifshay from comment #31)
>  
> > There's a simple solution, which you're missing because you're still trying
> > to cram ValueCastable into a Value-shaped hole where it doesn't fit -- a
> > ValueCastable *isn't* a Value
> 
> that you recommend this indicates that you do not understand the paradigm
> of the abstraction concept, at all.

no, I do understand it, but I'm saying ValueCastable is conveniently useful for a completely *separate* purpose than what UserValue and ValueCastable were originally designed for. ValueCastable is useful for that separate purpose where you have a python object that isn't a Value, shouldn't behave like a Value, doesn't have Value's API, etc. but you want it to be implicitly/explicitly convertible to a Value.

(also, you're coming across as implying i'm too stupid to understand right away so you will just continue doing what you want and disregard what I think -- please don't do that, it's not constructive)

>  it also explains why you keep
> recommending
> to duplicate the entire dsl.py source code.

no, that's a completely separate thing with separate reasoning having nothing to do with this....don't confuse them. again, simd value stuff is a different conversation that shouldn't be here -- we both agree it uses UserValue, the rest is irrelevant for smtlib2 support (smtlib2 won't be simd-ifyable for now).

I switched nmigen and yosys to the new rtlil API:
https://github.com/YosysHQ/yosys/pull/3319#issuecomment-1145606912
> I switched the implementation to use attributes on the outputs
> and an attribute on the module.
> 
> example:
> yosys/tests/various/smtlib2_module.v
> 
> Lines 1 to 10 in cd57c5a
> 
>  (* smtlib2_module *) 
>  module smtlib2(a, b, add, sub, eq); 
>  	input [7:0] a, b; 
>  	(* smtlib2_comb_expr = "(bvadd a b)" *) 
>  	output [7:0] add; 
>  	(* smtlib2_comb_expr = "(bvadd a (bvneg b))" *) 
>  	output [7:0] sub; 
>  	(* smtlib2_comb_expr = "(= a b)" *) 
>  	output eq; 
>  endmodule 
> I also added a test that compares the generated smt2 to the
> expected output, avoiding the need to run a smtlib2 solver (which
> iirc yosys doesn't want a dependency on)

I haven't yet backported the new yosys modifications to the yosys 0.13 branch, I'll do that after I get it working upstream.

I still need to make some modifications to sby:
* removing -simcheck:
https://github.com/YosysHQ/sby/issues/168
* adding support for cvc5 (both cvc4 and z3 fail on one of nmigen's new tests now):
https://github.com/YosysHQ/sby/issues/167

(In reply to Jacob Lifshay from comment #34)
> I still need to make some modifications to sby:
> * removing -simcheck:
> https://github.com/YosysHQ/sby/issues/168

I created a PR:
https://github.com/YosysHQ/sby/pull/170

> * adding support for cvc5 (both cvc4 and z3 fail on one of nmigen's new
> tests now):
> https://github.com/YosysHQ/sby/issues/167
Moved to:
https://github.com/YosysHQ/yosys/issues/3356

jix created a PR:
https://github.com/YosysHQ/yosys/pull/3357

(In reply to Jacob Lifshay from comment #34)
> I haven't yet backported the new yosys modifications to the yosys 0.13
> branch, I'll do that after I get it working upstream.

I backported the new yosys modifications. I did a force push because the new yosys modifications were completely rewritten and upstream most likely doesn't want a bunch of commits that do it one way then completely undo that and do it another way. I'm keeping the backported branch in sync.

I also got gitlab ci up and working with cvc5, sby from my fork (needed because my PR isn't yet merged), and other stuff.

(In reply to Jacob Lifshay from comment #34)
> I switched nmigen and yosys to the new rtlil API:
> https://github.com/YosysHQ/yosys/pull/3319

That PR has been merged!

(In reply to Jacob Lifshay from comment #37)
> (In reply to Jacob Lifshay from comment #34)
> > I switched nmigen and yosys to the new rtlil API:
> > https://github.com/YosysHQ/yosys/pull/3319
> 
> That PR has been merged!

ha, very cool.

https://git.libre-soc.org/?p=dev-env-setup.git;a=commitdiff;h=3066663eed414b7577d7dde2efcb62f9d0ca5733

jacob any chance you could make sure that the yosys hdl-tools-yosys
script stays up-to-date, we've just rather embarrassingly had a
new developer from the IBM-sponsored OpenPOWER Academic Development Group
fail to be able to install from the scripts.

(In reply to Luke Kenneth Casson Leighton from comment #39)
> https://git.libre-soc.org/?p=dev-env-setup.git;a=commitdiff;
> h=3066663eed414b7577d7dde2efcb62f9d0ca5733
> 
> jacob any chance you could make sure that the yosys hdl-tools-yosys
> script stays up-to-date, we've just rather embarrassingly had a
> new developer from the IBM-sponsored OpenPOWER Academic Development Group
> fail to be able to install from the scripts.

I could try, but as i don't use it myself (because imho the scripts take the wrong approach to installing/using software -- running as root and not using a venv among other things), i'm probably not the right person to maintain it.

(In reply to Jacob Lifshay from comment #40)

> I could try, but as i don't use it myself (because imho the scripts take the
> wrong approach to installing/using software -- running as root and not using
> a venv among other things), i'm probably not the right person to maintain it.

jacob they're unbelievably important to the project!

those scripts have saved new developers *weeks* because they
download and install hundreds of packages.

they should be your *very first* port of call and helping to keep
them up-to-date so that other people's lives can be made easier
should be your absolute top priority!

they are also the "reproducible build" scripts that ensure and
guarantee that every developer is reproducing the exact same
software development environment.

we cannot possibly submit GDS-II files to a Foundry, paying out
USD 16 million on masks when two developers have *different*
GDS-II files and it turns out they installed an untested library
because they didn't use the Project's official reproducible
build scripts

this is *really* fundamental. whether you *like* how they're
done is, sorry to have to say this, completely irrelevant
next to how absolutely critically important they are.

(In reply to Luke Kenneth Casson Leighton from comment #41)
> (In reply to Jacob Lifshay from comment #40)
> 
> > I could try, but as i don't use it myself (because imho the scripts take the
> > wrong approach to installing/using software -- running as root and not using
> > a venv among other things), i'm probably not the right person to maintain it.
> 
> they should be your *very first* port of call and helping to keep
> them up-to-date so that other people's lives can be made easier
> should be your absolute top priority!

I didn't say they aren't high priority, I said I'm probably the wrong person to maintain them. I can try to maintain them anyway if there isn't a better person.

(In reply to Jacob Lifshay from comment #42)

> I didn't say they aren't high priority, I said I'm probably the wrong person
> to maintain them. I can try to maintain them anyway if there isn't a better
> person.

ultimately here it comes down to responsibility.
a new command has been added (write_jby?) in the chain involving
symbiyosys, and that caused the fundamental developer
scripts that everyone critically relies on to break.

https://git.libre-soc.org/?p=dev-env-setup.git;a=commitdiff;h=3066663eed414b7577d7dde2efcb62f9d0ca5733

i fixed it this time because it was urgent (and embarrassing
to have to inform a high-profile developer, who is going
to test ls180 through Cadence VLSI tools for us, that we had failed
to keep the scripts up-to-date)

cvc5 is also going to need to be added to the decscripts,
asking veera to do that is probably the best thing there.

(In reply to Luke Kenneth Casson Leighton from comment #43)
> (In reply to Jacob Lifshay from comment #42)
> 
> > I didn't say they aren't high priority, I said I'm probably the wrong person
> > to maintain them. I can try to maintain them anyway if there isn't a better
> > person.
> 
> ultimately here it comes down to responsibility.
> a new command has been added (write_jby?) in the chain involving
> symbiyosys, and that caused the fundamental developer
> scripts that everyone critically relies on to break.

yeah, i should have thought to update everything else when I saw that sby master  had changed since those scripts were written -- i'm not the one who changed sby to need write_jny. this comes from relying on the master branch rather than a reliably-unchanging version such as a git tag or commit id.
> 
> https://git.libre-soc.org/?p=dev-env-setup.git;a=commitdiff;
> h=3066663eed414b7577d7dde2efcb62f9d0ca5733
> 
> i fixed it this time because it was urgent (and embarrassing
> to have to inform a high-profile developer, who is going
> to test ls180 through Cadence VLSI tools for us, that we had failed
> to keep the scripts up-to-date)
> 
> cvc5 is also going to need to be added to the decscripts,
> asking veera to do that is probably the best thing there.

yeah, i was mostly planning on waiting until the smtlib2 support is merged into nmigen, then we'd update everything at once to the known-to-work-from-ci versions on the 0.13-i-forgot-the-name branch.

(In reply to Jacob Lifshay from comment #44)
> yeah, i should have thought to update everything else when I saw that sby
> master  had changed since those scripts were written -- i'm not the one who
> changed sby to need write_jny.

that happened in https://github.com/YosysHQ/sby/pull/140, before I even started on smtlib2 stuff.

As described in:
https://libre-soc.org/irclog/%23libre-soc.2022-06-16.log.html?PageSpeed=noscript#t2022-06-16T03:15:24

I think we should wait for https://github.com/YosysHQ/sby/pull/170 to merge before we update the yosys/nmigen/sby dev-env-setup scripts. We need something (icr what right now) in sby master that's not in that PR, and that PR. I want to use the merge commit (or a later commit in sby) that will be created in sby master, rather than creating our own in a fork.

(In reply to Jacob Lifshay from comment #46)
> As described in:
> https://libre-soc.org/irclog/%23libre-soc.2022-06-16.log.
> html?PageSpeed=noscript#t2022-06-16T03:15:24
> 
> I think we should wait for https://github.com/YosysHQ/sby/pull/170 to merge
> before we update the yosys/nmigen/sby dev-env-setup scripts. We need
> something (icr what right now) in sby master that's not in that PR, and that
> PR. I want to use the merge commit (or a later commit in sby) that will be
> created in sby master, rather than creating our own in a fork.

there's only *three months* left on the clock before 75% of the money available
from NLnet is terminated due to Horizon 2020 ending.

waiting even 2 weeks is 15% - *one sixth* - of the available time.

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"

basically i am strongly, strongly hinting that "waiting" is a really bad idea.

i've created a SymbiYosys repo.

(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.

(In reply to Jacob Lifshay from comment #48)

> 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.

doesn't matter, the opportunity is to get something in ASAP well before
the october 1st deadline.

we *must* not leave it to the absolute last minute: NLnet themselves
have a cut-off point where they will not receive the money from the EU
even if an RFP is submitted to them.

>   Blocked on: https://github.com/YosysHQ/sby/pull/170

please reference this pull request in the dev-env-setup
scripts and progress on this immediately.

we *cannot wait* on other people to take action.

veera can you track down what that is, update hdl-tools-yosys
and the git.libre-soc.org SymbiYosys repository with the
appropriate branch/tag

i've added you with write permissions to these:

https://git.libre-soc.org/?p=SymbiYosys.git;a=summary
https://git.libre-soc.org/?p=yosys.git;a=summary

(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.

(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

(In reply to Jacob Lifshay from comment #52)
> 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 

whoops, I forgot the rest of the sentence. it should work by using the
add-simcheck-option branch:
https://git.libre-soc.org/?p=SymbiYosys.git;a=shortlog;h=refs/heads/add-simcheck-option

https://github.com/YosysHQ/yosys/pull/3391 was merged, so now all we're waiting on for upstream yosys/sby is https://github.com/YosysHQ/sby/pull/170 which requires at least 1 day wait for the tools including yosys#3391 to be updated so sby's CI passes.

https://github.com/YosysHQ/sby/pull/170 was merged, so all we're waiting on now is nmigen upstream (aka. lkcl) -- i want to wait for the ci tests to pass for yosys/sby master before merging the nmigen merge request...running ci now.

also i want to change the .gitlab-ci.yml to fix the comments about switching back to sby upstream...the 0.13 branch test will use master of libre-soc's sby repo.

(In reply to Jacob Lifshay from comment #55)
> https://github.com/YosysHQ/sby/pull/170 was merged, so all we're waiting on
> now is nmigen upstream (aka. lkcl) -- i want to wait for the ci tests to
> pass for yosys/sby master before merging the nmigen merge request...running
> ci now.
> 
> also i want to change the .gitlab-ci.yml to fix the comments about switching
> back to sby upstream...the 0.13 branch test will use master of libre-soc's
> sby repo.

done. i also updated libre-soc's sby repo. afaict the nmigen merge request is ready to be merged.

brilliant, there's one thing left that needs doing, the
patch to ValueCastable to override __dict__ can you please
extract that as its own atomic commit with its own identifiable
commit message.

anything else that is modifications to existing nmigen source
code please do the same with a clear explanation.

it is really important that critical changes to the nmigen API
not end up "hidden"

(In reply to Luke Kenneth Casson Leighton from comment #57)
> brilliant, there's one thing left that needs doing, the
> patch to ValueCastable to override __dict__ can you please
> extract that as its own atomic commit with its own identifiable
> commit message.
> 
> anything else that is modifications to existing nmigen source
> code please do the same with a clear explanation.
> 
> it is really important that critical changes to the nmigen API
> not end up "hidden"

Ok, I rewrote all the commits, squashing them into just a few commits, with modifications to ValueCastable and the rest of nmigen split out as their own commits.

The old commits are at:
https://gitlab.com/programmerjake/nmigen/-/tree/smtlib2-expr-support-old