Problems with 3 bit add not passing eqy

[oharboe]

Version

Yosys 0.43 (git sha1 ead4718e5, g++ 13.2.0-23ubuntu4 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

I realize this is not the shortest possible test-case for this problem, but it is a standalone test-case with everything needed to reproduce it. Thanks to @hovind for figuring this out. This was discovered while working with OpenROAD on ASAP7.

To reproduce:

untar https://drive.google.com/file/d/1x1WbP7VeAsBBjP4zuXUaUmnka_AikNCp/view?usp=sharing

Then run:

./run-me-adder-asap7-base.sh

Output:

26. Executing Verilog backend.
Dumping module `\adder'.

End of script. Logfile hash: f8c4509b61, CPU: user 1.16s system 0.05s, MEM: 132.97 MB peak
Yosys 0.43 (git sha1 ead4718e5, g++ 13.2.0-23ubuntu4 -fPIC -Os)
Time spent: 24% 6x read_liberty (0 sec), 23% 2x stat (0 sec), ...
+ eqy -d ./logs/asap7/adder/base/4_eqy_output --force ./objects/asap7/adder/base/1_2_test.eqy
+ tee ./logs/asap7/adder/base/1_2_test.txt
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] read_gold: starting process "yosys -ql ./logs/asap7/adder/base/4_eqy_output/gold.log ./logs/asap7/adder/base/4_eqy_output/gold.ys"
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] read_gold: finished (returncode=0)
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] read_gate: starting process "yosys -ql ./logs/asap7/adder/base/4_eqy_output/gate.log ./logs/asap7/adder/base/4_eqy_output/gate.ys"
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] read_gate: finished (returncode=0)
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] combine: starting process "yosys -ql ./logs/asap7/adder/base/4_eqy_output/combine.log ./logs/asap7/adder/base/4_eqy_output/combine.ys"
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] combine: finished (returncode=0)
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] partition: starting process "cd ./logs/asap7/adder/base/4_eqy_output; yosys -ql partition.log partition.ys"
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] partition: finished (returncode=0)
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: starting process "make -C ./logs/asap7/adder/base/4_eqy_output -f strategies.mk"
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: make: Entering directory '/home/oyvind/OpenROAD-flow-scripts/flow/foo/logs/asap7/adder/base/4_eqy_output'
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: Running strategy 'basic' on 'adder.io_dst'..
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: Could not prove equivalence of partition 'adder.io_dst' using strategy 'basic'
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: make -f strategies.mk summary
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: make[1]: Entering directory '/home/oyvind/OpenROAD-flow-scripts/flow/foo/logs/asap7/adder/base/4_eqy_output'
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: make[1]: Leaving directory '/home/oyvind/OpenROAD-flow-scripts/flow/foo/logs/asap7/adder/base/4_eqy_output'
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: make: Leaving directory '/home/oyvind/OpenROAD-flow-scripts/flow/foo/logs/asap7/adder/base/4_eqy_output'
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] run: finished (returncode=0)
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] Warning: Failed to prove equivalence for 1/1 partitions:
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] Failed to prove equivalence of partition adder.io_dst
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
EQY  2:05:25 [./logs/asap7/adder/base/4_eqy_output] DONE (FAIL, rc=2)

Expected Behavior

no failure in eqy

Actual Behavior

failure

[oharboe]

Is this another manifestation of https://github.com/YosysHQ/yosys/issues/3879 ?

[oharboe]

@QuantamHD @maliberty FYI