Default partitioning of eqy fails to prove equivalence for circuit containing only "eq" and "neq", but succeeds if output is turned into internal wire about eqy

[edwintorok]

FWIW adding this to equiv.eqy makes the proof work, but that feels more like a workaround (aigmap on its own is not enough, it needs the opt too):

aigmap
opt

workaround equiv.eqy:

[gold]
read_verilog gold.v
prep -top comparators
aigmap
opt

[gate]
read_verilog gate.v
prep -top comparators
aigmap
opt

[strategy sby]
use sby
depth 10
engine smtbmc z3

[jix]

This is not a bug in SBY, but a known current limitation of EQY's partitioning that we plan to improve on. When EQY passes a partition to SBY, that partition is checked in isolation, that's a core part of EQY's design, but it requires that the partitioning is done in a way that equality can still be proved. Our current partitioning code often requires some manual tuning to ensure that this is possible. In this case EQY decided to split the partitions in such a way that when checking that the gold side neq = a != b matches the gate side neq = ~eq the common logic that defines eq itself is not part of the partition. This means while checking the partition neq, it treats a, b and eq as unknowns, in which case eq == neq becomes possible without the context of the logic outside of the partition.

During partition EQY prints the following warnings as it couldn't perfectly align both sides due to structural changes between gold and gate, which is an indicator that such a problem might be present, especially if it's present for both gold and gate inputs for the same partition.

EQY 15:32:56 [equiv] Warning: Partition comparators.neq contains 1 unused gold inputs.
EQY 15:32:56 [equiv] Warning: Partition comparators.neq contains 2 unused gate inputs.

In this case I could pinpoint the problem just from the observed behavior and log output, but in general the directory created by eqy contains more detailed log, data and RTLIL files that can help diagnosing such issues, especially for larger designs.

One workaround that directly addresses this underlying reason for the false-positive equivalence-failure is to explicitly tell EQY to make the definition of eq available whenever it is used, even across a partition boundary, by adding the following section to the .eqy file:

[partition comparators]
amend eq

[jix]

Actually I'll keep this issue open, even if requiring manual annotations is currently by design, as we do plan to improve this and keeping track of examples where the current approach doesn't do the right thing automatically is useful for that.

[edwintorok]

Thanks, the amend works. In fact this works too and is not design specific (so far I'm only using sby/eqy to prove the equiv of really small designs and was looking for a way to turn partitioning 'off', obviously for larger designs I'll have to annotate by hand):

 [partition *]
 amend *

Am I understanding correctly that whenever I see this warning Warning: Partition comparators.neq contains ... unused ... inputs.: I have to find out the names of those inputs and add an amend entry with that signal name? In which case having the warning print the list of signal names that are unconnected might be useful.