Skip to content

Comparing post-synth netlists fails sec #204

Open
Open
Comparing post-synth netlists fails sec#204

Description

@jeffng-or
jeffng-or
opened on Aug 13, 2026

I'm trying to compare two post-synth netlists: one where clock gates are inferred and one where the clock gates are not inferred. SEC is reporting a difference, so I'm not sure if it's an issue in kepler-formal or in yosys clockgate.

I've captured the output after setting the KEPLER_SEC_DIAG and KEPLER_SEC_PDR_TRACE env vars.

The nangate45 based example is attached.

infer.v.txt
miter_log_0.txt
no_infer.v.txt
output.log
verify.yml.txt

Activity

  1. nanocoh commented on Aug 22, 2026

    @nanocoh
    nanocoh
    on Aug 22, 2026
    Contributor

    hi @jeffng-or , This issue heppend due to mistreatment of latches in this desing by the tool which is now fixed in main. Can you check again the diff is gone with latest?

  2. jeffng-or commented on Aug 24, 2026

    @jeffng-or
    jeffng-or
    on Aug 24, 2026
    Author

    With a1a56e9, I'm getting an inconclusive result:

    [2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1829] KEPLER FORMAL: Run.
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1844] Input format: VERILOG
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1846] Run log: miter_log_3.txt
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:692] Netlist 1: infer.v
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:692] Netlist 2: no_infer.v
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1994] Solver: KISSAT
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1995] Verification: sec
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1997] SEC max_k: 32
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1998] SEC engine: pdr
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:1999] SEC encoding: dual_rail_steady
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2001] Compact mode: disabled
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2002] Skipped PO reports: disabled
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2004] Library: /workspace/kf_main/OpenROAD-flow-scripts/flow/platforms/nangate45/lib/NangateOpenCellLibrary_typical.lib
[2026-08-24 15:44:23.180] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2176] Loading library file: /workspace/kf_main/OpenROAD-flow-scripts/flow/platforms/nangate45/lib/NangateOpenCellLibrary_typical.lib
[2026-08-24 15:44:23.234] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2543] Parsing verilog file(s) for design 1
[2026-08-24 15:44:23.235] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2590] Found top design: clkgate_test
[2026-08-24 15:44:23.235] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2176] Loading library file: /workspace/kf_main/OpenROAD-flow-scripts/flow/platforms/nangate45/lib/NangateOpenCellLibrary_typical.lib
[2026-08-24 15:44:23.281] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2662] Parsing verilog file(s) for design 2
[2026-08-24 15:44:23.282] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2701] Found top design: clkgate_test
[2026-08-24 15:44:23.297] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2022] SEC checked-output coverage: 19.05% (4/21 covered/existing outputs).
[2026-08-24 15:44:23.297] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2051] SEC skipped observed outputs due to extraction or coverage limitations:
  - data_out[0]: design0 opaque-internal: Depends on skipped state `data_reg[0]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - data_out[1]: design0 opaque-internal: Depends on skipped state `data_reg[1]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - data_out[2]: design0 opaque-internal: Depends on skipped state `data_reg[2]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - data_out[3]: design0 opaque-internal: Depends on skipped state `data_reg[3]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - data_out[4]: design0 opaque-internal: Depends on skipped state `data_reg[4]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - data_out[5]: design0 opaque-internal: Depends on skipped state `data_reg[5]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - data_out[6]: design0 opaque-internal: Depends on skipped state `data_reg[6]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - data_out[7]: design0 opaque-internal: Depends on skipped state `data_reg[7]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - count_out[0]: design0 opaque-internal: Depends on skipped state `count_reg[0]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - count_out[1]: design0 opaque-internal: Depends on skipped state `count_reg[1]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - count_out[2]: design0 opaque-internal: Depends on skipped state `count_reg[2]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - count_out[3]: design0 opaque-internal: Depends on skipped state `count_reg[3]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - single_out[0]: design0 opaque-internal: Depends on skipped state `single_bit$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_40_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - always_out[0]: design0 opaque-internal: Depends on skipped state `always_reg[0]$_DFF_PN0_.Q[0]`: Depends on skipped state `count_reg[0]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - always_out[1]: design0 opaque-internal: Depends on skipped state `always_reg[1]$_DFF_PN0_.Q[0]`: Depends on skipped state `count_reg[1]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - always_out[2]: design0 opaque-internal: Depends on skipped state `always_reg[2]$_DFF_PN0_.Q[0]`: Depends on skipped state `count_reg[2]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)
  - always_out[3]: design0 opaque-internal: Depends on skipped state `always_reg[3]$_DFF_PN0_.Q[0]`: Depends on skipped state `count_reg[3]$_DFFE_PN0P_.Q[0]`: Sequential clock pin was skipped because opaque internal cell `_41_` (model `CLKGATE_X1`) pin `GCK[0]`: combinational truth table arity does not match instance inputs (TT arity=0, instance input count=2)

[2026-08-24 15:44:23.297] [kepler_formal_main_logger] [info] [KeplerFormal.cpp:2095] SEC partially proved equivalence at k = 1: 4/21 outputs proved; remaining outputs are inconclusive.
[2026-08-24 15:44:23.297] [kepler_formal_main_logger] [warning] [KeplerFormal.cpp:2101] SEC verification did not prove all observed outputs.

    Are you seeing the same with the test case I previously included? Thanks!

  3. nanocoh commented on Aug 27, 2026

    @nanocoh
    nanocoh
    on Aug 27, 2026
    Contributor

    hello @jeffng-or,

    I approve I see the same.

    Currently we have ongoing work to support latches for SEC(no problems in LEC) which is aiming to solve the origin of the partial proof here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions