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

[edwintorok]

This is the smallest reproducer for the bug, given modules gate.v:

module comparators (
    b,
    a,
    eq,
    neq
);
    input [7:0] b;
    input [7:0] a;
    output eq;
    output neq;

    assign eq = a == b;
    assign neq = ~eq;
endmodule

and gold.v:

module comparators (
    b,
    a,
    eq,
    neq
);
    input [7:0] b;
    input [7:0] a;
    output eq;
    output neq;

    assign eq = a == b;
    assign neq = a != b;
endmodule

sby claims that the neq partitions are not equivalent. In the generated .vcd trace both eq and neq are shown with value 1 for gold.v which doesn't make sense, those 2 should always be a negation of each-other.

If I change eq to be a wire instead of an output then suddenly it is able to prove that neq is in fact equivalent.
(Note that introducing additional wires in gate.v doesn't help either).
I tried several smtbmc engines (bitwuzla, boolector) with the same result, the problem seems to be with the way the partition is created.

Reproduced the bug with oss-cad-suite-linux-x64-20230821.tgz running on Fedora 38.

I've attached the full working and failing inputs and the full logs created by eqy:
sbybug.zip

The warning about unconnected inputs here looks suspicious:

EQY 22:33:27 [equiv] read_gold: starting process "yosys -ql equiv/gold.log equiv/gold.ys"
EQY 22:33:27 [equiv] read_gold: finished (returncode=0)
EQY 22:33:27 [equiv] read_gate: starting process "yosys -ql equiv/gate.log equiv/gate.ys"
EQY 22:33:27 [equiv] read_gate: finished (returncode=0)
EQY 22:33:27 [equiv] combine: starting process "yosys -ql equiv/combine.log equiv/combine.ys"
EQY 22:33:27 [equiv] combine: finished (returncode=0)
EQY 22:33:27 [equiv] partition: starting process "cd equiv; yosys -ql partition.log partition.ys"
EQY 22:33:27 [equiv] partition: finished (returncode=0)
EQY 22:33:27 [equiv] Warning: Partition comparators.neq contains 1 unused gold inputs.
EQY 22:33:27 [equiv] Warning: Partition comparators.neq contains 2 unused gate inputs.
EQY 22:33:27 [equiv] run: starting process "make -C equiv -f strategies.mk"
EQY 22:33:27 [equiv] run: make: Entering directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: Running strategy 'sby' on 'comparators.eq'..
EQY 22:33:27 [equiv] run: Proved equivalence of partition 'comparators.eq' using strategy 'sby'
EQY 22:33:27 [equiv] run: Running strategy 'sby' on 'comparators.neq'..
EQY 22:33:27 [equiv] run: Could not prove equivalence of partition 'comparators.neq' using strategy 'sby': partitions not equivalent
EQY 22:33:27 [equiv] run: make -f strategies.mk summary
EQY 22:33:27 [equiv] run: make[1]: Entering directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: make[1]: Leaving directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: make: Leaving directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: finished (returncode=0)
EQY 22:33:27 [equiv] Successfully proved equivalence of partition comparators.eq
EQY 22:33:27 [equiv] Warning: Failed to prove equivalence for 1/2 partitions:
EQY 22:33:27 [equiv] Failed to prove equivalence of partition comparators.neq
EQY 22:33:27 [equiv] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
EQY 22:33:27 [equiv] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
EQY 22:33:27 [equiv] DONE (FAIL, rc=2)

What am I doing wrong?

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