equiv_make: Add -assert option

[georgerennie]

This adds an -assert flag to equiv_make. When used, the pass generates $eqx and $assert cells to encode equivalence instead of $equiv, which means the equivalence check can be done with SymbiYosys. As these assertions are at the word level, they typically solve faster with SymbiYosys than using equiv_induct in yosys, at the cost of less helpful error messages.

I'm not certain on the name of the option as -assert is used in some other commands to mean that the command should produce an error if it fails which is different to its meaning here

You can also do something similar to this by using equiv_make followed by equiv_miter -assert, however the assertions resulting from this are all one bit wide (as they are derived from equiv cells which are always only 1 bit). In my experiments these took significantly longer to solve than generating equivalences at the word level.

I'm happy to make any changes as needed to make it more usable/fit the yosys codebase style more etc (or if its an already existing feature i've somehow missed)

[jix]

As far as I can tell, your equiv_make -assert gold gate equiv_make is the same as miter -equiv -make_assert gold gate miter_equiv (apart from the latter not flattening gold and gate). Let me know if I missed any other difference.

Also note that in general the check used by $equiv is not quite the same asserting $eqx. For $equiv when the A input is x, any value for B is accepted. Such a check can also be created via miter by adding the -ignore_gold_x flag. While this matters in simulation, for sby that makes no difference as it does not consider x as a separate value distinct from 0 and 1 but rather as an unknown/unconstrained value.

[georgerennie]

It's been a while since I worked on this so I may be misremembering parts (and I think looking at it now there are some bits that could be tidied up/may be a little buggy), but the main reasoning I had for it was that using miter doesn't (as far as I've been able to use it) create any equivalence relations internally (as you say it doesn't flatten the design).

Since having some of these internal equivalences can decrease the time to prove two circuits equivalent, the main idea behind this PR was to be able to do this type of checking at the word level instead of bit level (as $equiv cells are single bit and equiv_induct is SAT based instead of SMT) whilst retaining those internal equivalences, leading to faster solving with sby (additionally sby has the abc pdr engine and others that are often faster than equiv_induct).

Your points about $eqx are very much correct and it could be replaced by an $eq cell. There's also a few other things that I would want to look at again with this, like the fact that it doesn't pass outputs through to the outputs of the miter module.

[jix]

Ah, I forgot about internal equivalence checks and only tested it with a design that was too simple to show a difference here. Regarding $equiv vs $eqx and $eq, also $eq is not the same as $equiv. For -ignore_gold_x the miter pass generates logic emulating $equiv by comparing each individual bit to x to ignore bits where gold has an x value but to still fail when only gate has an x. That of course defeats the advantage of having word-level equivalences. I think using $eqx is fine as long as that difference is properly documented.

[georgerennie]

Ahh that all makes sense. I am a bit busy at the moment but in a week or two I have some more time so I will have a look then at documenting those differences (it would be nice to get the semantics as close to a drop-in replacement for $equiv as possible, modulo the lack of x support in sby) and tidying the PR up a bit so its more mergeable.

[georgerennie]

I've tidied things up a bit, and renamed it to -make_assert in line with miter and other commands. I have also added a test.

On the topic of exactly how to encode equivalence I had a few thoughts. miter -make_assert -ignore_gold_x and simlib use assert(A === 'x || A === B) for each bit. This makes sense for simulation with x support, however doesn't make a ton of sense for formal focused environments. Although when used as an assertion this will not supress assertion failures, if converted to an assumption it allows the value of A to be unconstrained. By comparison, miter -make_assert uses assert(A === B) which is better suited to formal and clearer.

I debated adding the -ignore_gold_x option to equiv_make as well to allow the user to choose between the two, but I think it would be of little practical use, as the main benefit of using equiv_make -make_assert over miter -make_assert for formal is that internal equivalences make equivalence checking faster, something that is not true for simulation. Thus I think simulation equivalence checking is better suited by just using a miter, or alternatively using equiv_make with the simlib version of $equiv.

Therefore this PR just implements the $eqx based semantics and I have tried to make this clear in the option description.