Hello everyone. I added "LEC_ENABLE" : 1 to config.json and run "make user_project_wrapper". Then ERROR happened as below. Before adding LEC_ENABLE, "make user_project_wrapper" works without any problem. Why does this error happen? [STEP 9] [INFO]: Running Placement Resizer Design Optimizations (log: ../home/harada/Project/011_OpenLane/caravel_test_005_ram2/openlane/user_project_wrapper/runs/24_05_21_16_21/logs/placement/9-resizer.log)... [STEP 10] [INFO]: Running LEC: '../home/harada/Project/011_OpenLane/caravel_test_005_ram2/openlane/user_project_wrapper/runs/24_05_21_16_21/results/synthesis/user_project_wrapper.v' vs. '../home/harada/Project/011_OpenLane/caravel_test_005_ram2/openlane/user_project_wrapper/runs/24_05_21_16_21/tmp/placement/9-resizer.nl.v' (log: ../home/harada/Project/011_OpenLane/caravel_test_005_ram2/openlane/user_project_wrapper/runs/24_05_21_16_21/logs/10-synthesis.equiv.log)... [ERROR]: during executing yosys script /openlane/scripts/yosys/logic_equiv_check.tcl [ERROR]: Log: ../home/harada/Project/011_OpenLane/caravel_test_005_ram2/openlane/user_project_wrapper/runs/24_05_21_16_21/logs/10-synthesis.equiv.log [ERROR]: Last 10 lines: Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13797: \_0478__gold \_0478__gate Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13800: \_0475__gold \_0475__gate Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13802: \_0473__gold \_0473__gate Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13804: \_0471__gold \_0471__gate Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13806: \_0469__gold \_0469__gate Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13808: \_0467__gold \_0467__gate Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13810: \_0465__gold \_0465__gate Unproven $equiv $auto$equiv_make.cc:294:find_same_wires$13812: \_0463__gold \_0463__gate Unproven $equiv $auto$equiv_mERROR: Found 257 unproven $equiv cells in 'equiv_status -assert'. child process exited abnormally [ERROR]: Creating issue reproducible... [INFO]: Saving runtime environment... OpenLane TCL Issue Packager

@Yomei Harada Looks like the logic equivalency check is failing. Here’s a sample result

Trying to prove $equiv cell $auto$<http://equiv_make.cc:257:find_same_wires$13266|equiv_make.cc:257:find_same_wires$13266>:
    A = \<http://_1804__gold.IQ|_1804__gold.IQ>, B = \<http://_1804__gate.IQ|_1804__gate.IQ>, Y = \wbs_ack_o
    Adding 0 new cells to the problem (0 A, 0 B, 0 shared).
    Problem size at t=10: 8 literals, 12 clauses
    Failed to prove equivalence with sequence length 0.
    No nets to continue in previous time step.

I’m not familiar with the LEC check output, but I believe it’s comparing a gate level verilog netlist before optimization to a gate leve verilog netlist after optimization. It seems that that the original and anything that matches the original has a

_gold

suffix, while things that don’t match in the optimized netlist have a

_gate

suffix. Maybe you can trace from the source of the

wbs_ack_o

signal and see if you can spot the difference.

@Mitch Bailey Thank you for your reply. I have a question. I think equivalence check between verilog-RTL vs final netlist is mandatory. But openlane.log doesn't have equivalence check information. Does openlane flow have equivalence check in default?

@Yomei Harada I’m not sure. @donn?

The LEC feature is quite buggy and finicky to set up. We don't use it for our own designs, favoring thorough gate-level simulation.