Yosys Equivalence check fails beween Synthesis and CTS file

[dineshannayya]

Hi

I am trying do LEC between synthesised netlist Vs CTS netlist. I see tool not able to match clock tree nets.

Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9872: \sdram_clk \clknet_6_15_0_sdram_clk_gate
Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9876: \wb_clk_i \clknet_6_51_0_wb_clk_i_gate
Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9880: \wb_clk_i \clknet_6_49_0_wb_clk_i_gate
Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9884: \wb_clk_i \clknet_6_49_0_wb_clk_i_gate
Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9888: \wb_clk_i \clknet_6_49_0_wb_clk_i_gate
Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9892: \wb_clk_i \clknet_6_53_0_wb_clk_i_gate
Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9896: \wb_clk_i \clknet_6_53_0_wb_clk_i_gate
Unproven $equiv $auto$equiv_make.cc:359:find_same_cells$9900: \wb_clk_i \clknet_6_53_0_wb_clk_i_gate

How to manage this

I have attached the example setup and
run command ./lec.tcl
log file is available at: output/yosys.equiv.log

I see same issue in latest yosys version

 Yosys 0.9+4270 (git sha1 539d4ee90, clang 10.0.0-4ubuntu1 -fPIC -Os)

exp1.tar.gz