Experimental: --skip-gated-clock-flops, so a clock-gated netlist can be checked, minus its gated flops

[oharboe]

Experimental: --skip-gated-clock-flops, so a clock-gated netlist can be checked, minus its gated flops

What this is for: a strong, cheap signal in automated loops (generate a netlist, LEC it, iterate). It is not a production clock-gating check. The option is off by default and logs a warning whenever it is used.

The problem

A flop clocked through an integrated clock gate cannot be compared today. Take a register file written through one clock gate per word:

• The gate netlist's flop has D = wdata and a gated clock.
• The RTL's flop has D = we ? wdata : q and the free clock.

kepler-formal makes the ICG's latch opaque, on purpose (Asap7StateFunctionClockGateIsOpaque), so its GCLK cannot be turned into an enable. The combinational check therefore reports a difference for every gated flop, and nothing else in the design gets a verdict.

What the option does

With --skip-gated-clock-flops (or skip_gated_clock_flops: true in a config file), BuildPrimaryOutputClauses leaves out the inputs of each sequential instance whose clock pin is driven by a cell output with:

• no truth table, and
• a combinational dependency on its cell's inputs.

That is how an ICG's GCLK comes out of a liberty statetable. A buffer has a truth table, and a clock divider's flop output has no combinational inputs, so neither matches.

The new skip reason is GatedClock:

• It is decided per output, before outputs sharing an iso get a representative, so a skip never reaches an output that is not a gated flop's.
• A warning gives the count, and with --report-skipped-pos the list goes to skipped_gated_clock_pos.txt.
• The miter already drops a pair when either side is invalid, so nothing else changes.

Everything else is still compared, which for a register file means every read through every flop's output. The write enable that moved onto the clock is the one thing not proven; simulation or a real clock-gate model has to cover it.

Tested

• MiterTests.SkipGatedClockFlopsLeavesOutOnlyFlopsClockedThroughAnIcg: an asap7-style ICG gating one DFF, a second DFF on the free clock. With the option, only the gated flop is skipped, with reason GatedClock. Without it, nothing is skipped for that reason. Asap7StateFunctionClockGateIsOpaque still passes, so the default modelling is unchanged.
• The full suite passes.
• Downstream, in bazel-orfs, OpenROAD's generate_regfile register files are checked against yosys's synthesis of their RTL in both write styles: 21 cases, including 7-write-port, banked and interleaved files. A deliberately wrong read path in a clock-gated file is still caught.

Not done

This does not model clock gates. A real fix would read clock_gating_integrated_cell from the liberty and turn GCLK = CLK & (ENA | SE) into a flop enable, in both the combinational and sequential checks. That needs Naja to keep the attribute. This option is a stopgap until then.

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 93.93939% with 4 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
src/bin/KeplerFormal.cpp	60.00%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!