Cannot verify a design with sec that lec says is equivalent

[jeffng-or]

I'm comparing two gate-level netlists:

1. netlist which has been technology mapped from a source technology - just swapped gates - gate mapping equivalency checked with KF
2. netlist which has been synthesized using the target library

When I run the design through with "lec", KF reports the designs are equivalent:

[2026-08-06 22:02:58.959] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2700] Found top design: gcd
[2026-08-06 22:02:59.225] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2851] No difference was found.

When I run using "sec", KF reports that the result is inconclusive:

[2026-08-06 22:03:38.908] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2006] SEC checked-output coverage: 61.11% (11/18 covered/existing outputs).
[2026-08-06 22:03:38.908] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2035] SEC skipped observed outputs due to extraction or coverage limitations:
  - req_rdy[0]: dual-rail PDR steady-state proof was inconclusive
  - resp_msg[0]: dual-rail PDR steady-state proof was inconclusive
  - resp_msg[8]: dual-rail PDR steady-state proof was inconclusive
  - resp_msg[9]: dual-rail PDR steady-state proof was inconclusive
  - resp_msg[11]: dual-rail PDR steady-state proof was inconclusive
  - resp_msg[12]: dual-rail PDR steady-state proof was inconclusive
  - resp_msg[13]: dual-rail PDR steady-state proof was inconclusive

[2026-08-06 22:03:38.908] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2094] SEC partially proved equivalence at k = 7: 11/18 outputs proved; remaining outputs are inconclusive.
[2026-08-06 22:03:38.908] [kepler_formal_main_logger] [warning] [KeplerFormal.cpp:2100] SEC verification did not prove all observed outputs.
[2026-08-06 22:03:38.908] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2103] SEC partial-proof details: Exact dual-rail PDR proved 11 of 18 observed outputs; remaining outputs are inconclusive

Can you provide some user-actionable messages to help identify where the differences are?

Here are the files for the test case:

1_2_yosys.v.txt
gt2n_gcd.v.txt
native_gt2n_lec.sh.txt

You can get the gt2n liberty files from: https://github.com/The-OpenROAD-Project/OpenROAD-flow-scripts/tree/master/flow/platforms/gt2n/lib

[nanocoh]

Hi @jeffng-or,

I will look at the test. Just to calrify the message of the SEC. 11/18 were proved equivalent. The rest of the terms were inconclusive.

It can happen in some cases where part of the flops are not set at boot.

For some more backround, SEC is looking at the top outputs while LEC looking at the seq bounary(all terms of seq elements + ffs but with harder assumption on the design), therefore there can be a difference in the result.