SEC: a design is not proven equivalent to itself, non-monotonically in the number of unrelated outputs #250

Summary

Passing the same file as --design1 and --design2 should be the easiest
possible SEC query: the two sides are byte-identical, so every output is
equivalent by construction. On an 8-register design this returns
87.50% (7/8), with dout[5] reported as
dual-rail PDR steady-state proof was inconclusive.

Verified on main (0ce1f2eb) and on f70c2e3: both builds give identical
results at every size tried, including which outputs come back inconclusive.

The result is deterministic for a given design, but varies
non-monotonically with the number of logically independent outputs beside
it: 4, 5, 6, 9, 16, 24 and 32 accumulators all prove, while 7, 8, 10 and 12 do
not. The accumulators do not interact, so whether dout[5] is proven depends on
how many unrelated registers happen to sit next to it.

Reproducer

Fully self-contained: one 33-line file, no PDK, no Liberty, ~20 s.

This needs the SystemVerilog frontend. The -verilog frontend is a structural
netlist parser — it rejects input wire in the port list, and then
reg [7:0] acc0; — so it cannot express a behavioural design at all.

module top (
  input wire clk,
  input wire rst,
  input wire [7:0] din,
  output wire [7:0] dout
);
  reg [7:0] acc0;
  reg [7:0] acc1;
  reg [7:0] acc2;
  reg [7:0] acc3;
  reg [7:0] acc4;
  reg [7:0] acc5;
  reg [7:0] acc6;
  reg [7:0] acc7;
  always @(posedge clk) begin
    if (rst) acc0 <= 8'd0; else acc0 <= acc0 + din + 8'd0;
    if (rst) acc1 <= 8'd0; else acc1 <= acc1 + din + 8'd1;
    if (rst) acc2 <= 8'd0; else acc2 <= acc2 + din + 8'd2;
    if (rst) acc3 <= 8'd0; else acc3 <= acc3 + din + 8'd3;
    if (rst) acc4 <= 8'd0; else acc4 <= acc4 + din + 8'd4;
    if (rst) acc5 <= 8'd0; else acc5 <= acc5 + din + 8'd5;
    if (rst) acc6 <= 8'd0; else acc6 <= acc6 + din + 8'd6;
    if (rst) acc7 <= 8'd0; else acc7 <= acc7 + din + 8'd7;
  end
  assign dout[0] = ^acc0;
  assign dout[1] = ^acc1;
  assign dout[2] = ^acc2;
  assign dout[3] = ^acc3;
  assign dout[4] = ^acc4;
  assign dout[5] = ^acc5;
  assign dout[6] = ^acc6;
  assign dout[7] = ^acc7;
endmodule

kepler-formal -sv \
  --design1 acc8.sv --design2 acc8.sv \
  --sv_design1_top top --sv_design2_top top \
  -v sec --sec-engine pdr --report-skipped-pos

Expected: all 8 outputs proved (the two sides are the same file).

Actual:

SEC checked-output coverage: 87.50% (7/8 covered/existing outputs).
SEC skipped observed outputs due to extraction or coverage limitations:
  - dout[5]: dual-rail PDR steady-state proof was inconclusive
SEC partially proved equivalence at k = 8: 7/8 outputs proved; remaining outputs are inconclusive.

Characterization

Same generator, N independent 8-bit accumulators, each driving one output bit.
Default encoding (dual_rail_steady), --sec-engine pdr:

(Seconds from the main build; the f70c2e3 build gives the same pass/fail and
the same inconclusive outputs, a few seconds slower on the same machine.)

• Deterministic: N=8 run three times, identical result each time (dout[5]).

• Not a capacity wall: N=32 proves in 49 s while N=7 fails in 17 s.

• Not a proof-depth limit: --max-k 64 and --max-k 256 both give exactly
  the same 7/8 and the same dout[5], in the same time. The reported
  max_k: 32 is never the binding constraint.

• Naming the reset fixes it: adding
  --sec-reset-cycles 4 --sec-reset-port rst=1 proves all 8 outputs, and does so
  in less wall-clock than the default run spends failing — roughly a third
  less, two runs each on one machine and build.

• A free rst is what the default run struggles with: with the if (rst)
  branch removed entirely (accumulators never reset) it proves at N=8, N=32 and
  N=128. Note rst is a shared primary input, so both sides see the same value
  and the design is self-equivalent either way.

• The failure mode depends on the encoding, and binary is worse. With
  --sec-encoding binary the same design returns 0.00% (0/8) immediately
  (exit 2), skipping every output rather than one:

  - dout[0]: design0 depends on reset-unanchored internal state 99.Q[7] | design1 depends on reset-unanchored internal state 99.Q[7]
  ...
  SEC cannot run on this design pair: No aligned observed outputs remain after skipping
  

  Both sides name the same unanchored state, which is what you would expect —
  they are the same file. Worth noting because quoting either result alone
  understates it: one encoding proves 7 of 8, the other proves none.

What this is not

• Not a design error: the two sides are the same path on disk.
• Not free-initial-state semantics. If unconstrained initial state were the
  reason, the unreset variant would be the hard one; it is the easy one, and
  it proves at every size tried.
• Not nondeterminism: three consecutive runs agree exactly.
• Not scale: larger instances of the identical construction prove.
• Not proof depth: raising --max-k eightfold changes nothing.
• Not one encoding's quirk: both dual_rail_steady and binary fail, in
  different ways (7/8 and 0/8 respectively).

Why it matters

In an RTL-vs-synthesis flow the two sides are never identical, so incompleteness
that already shows up on identical inputs is a floor on what such a flow can
check — and, because it moves non-monotonically with unrelated logic, it is not
something a user can design around or predict from the size of the design.

--sec-reset-cycles / --sec-reset-port is an effective remedy here, and on
this design it is also cheaper than failing. Two things would make it more
useful:

1. The default path should not be erratically incomplete on a self-equivalent
   design. A user who has not found the reset flags sees an unexplained
   partial result whose shape depends on unrelated logic.
2. The bootstrap's cost needs to stay bounded as designs grow, since it is
   the only remedy on offer — a remedy that does not fit in memory on a large
   design leaves that design back on the erratic default path.

Suggested regression check

A self-compare is the only SEC query whose answer is known before it runs: both
sides are byte-identical, so 100% coverage is guaranteed by construction. That
makes it the only kind of case that can be gated on full coverage with no risk
of a false failure — and it generalises, since any design already in the suite
can be added as a self-compare.

regress/run_sec_strategies_regress.sh already has the right expectation
(expect-full-coverage). The case is a few lines of config:

format: systemverilog
verification: sec
sec_engine: pdr
input_paths:
  - [./examples/self_equivalence/acc8.sv]
  - [./examples/self_equivalence/acc8.sv]
sv_design1_top: top
sv_design2_top: top
report_skipped_pos: true
solver: kissat

One caveat, measured by running this case through that script: registered
with the expectation the SEC workflows resolve to by default, it passes at exit
0 while proving almost nothing.

SEC_POSITIVE_EXPECTATION resolves to expect-equivalent-or-partial or
allow-unset-state-inconclusive, and SEC_FULL_COVERAGE_EXPECTATION only
becomes expect-full-coverage when require_full_coverage is passed by hand.
That is reasonable where partial coverage may be legitimate, but it does mean a
self-compare has to pin expect-full-coverage explicitly to be worth anything.

Priority

This is not blocking us. At this size the reset-bootstrap flags are an
effective workaround and we have a path forward without a fix here. We would
rather see the issues we filed earlier — #214, #244 and #245 — prioritised ahead
of this one. No urgency from our side.

Environment

• kepler-formal main at 0ce1f2ebd135d89cc3082725a9e38457f12d029c
  (reports version: 0.5.0, naja version: 0.7.23, naja git hash: 83be8a9e)
• Also reproduced on f70c2e38592d704c8cccf68433b091e82c8118f0, which links the
  byte-identical naja runtime — so this is not a naja-engine difference.
• Linux x86-64
• --sec-engine pdr; both --sec-encoding dual_rail_steady (the default) and
  binary as tabled
• Run both directly and through regress/run_sec_strategies_regress.sh in a
  mirror of the repo layout, with the config above

repro-self-equivalence.tar.gz