Unable to prove that original gcd design and synthesized gcd design are logicaly equivalent

[leeway64]

EQY version

EQY v0.56

Steps to Reproduce

git clone https://github.com/The-OpenROAD-Project/OpenROAD-flow-scripts.git
git clone https://github.com/YosysHQ/yosys.git

Run synth.ys by running yosys synth.ys:

read_verilog OpenROAD-flow-scripts/flow/designs/src/gcd/gcd.v
synth -top gcd

write_verilog -noexpr -noattr synthesized.v

Run .eqy by running eqy .eqy:

[gold]
read_verilog -sv /home/leeway64/ucsc/capstone/yosys/techlibs/common/simcells.v
read_verilog /home/leeway64/computer-science/sandbox-2/OpenROAD-flow-scripts/flow/designs/src/gcd/gcd.v

[gate]
read_verilog -sv /home/leeway64/ucsc/capstone/yosys/techlibs/common/simcells.v
read -sv synthesized.v

[script]
hierarchy -check -top gcd
prep
memory_map
extract_fa
async2sync

[strategy simple]
use sat
depth 10

[strategy sby]
use sby
depth 2
engine smtbmc bitwuzla

Expected Behavior

EQY should say that the original design and the synthesized design are logically equivalent.

Actual Behavior

At the end of the eqy's command output, I see that there are three partitions that are not equivalent:

Failed to prove equivalence of partition gcd.ctrl.statein_
Failed to prove equivalence of partition gcd.ctrl.b_reg_en
Failed to prove equivalence of partition gcd.ctrl.a_mux_sel

Am I not using EQY correctly? Are there specific commands I'm supposed to run in the script section to clean up the circuit before running logical equivalence? Does anyone have any tips for how to debug logical equivalence checking?

Thanks, I'd appreciate any and all help!

[oharboe]

Same thing? #88