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

[ovebryne]

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:

N	4	5	6	7	8	9	10	12	16	24	32
proved	all	all	all	6/7	7/8	all	8/10	11/12	all	all	all
inconclusive	–	–	–	dout[5]	dout[5]	–	dout[5], dout[9]	dout[10]	–	–	–
seconds	1	4	3	17	19	16	29	38	21	37	49

(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.

expectation	encoding	proved	script exit
allow-unset-state-inconclusive	binary	0/8	0 — passes
expect-equivalent-or-partial	dual_rail_steady	7/8	0 — passes
expect-full-coverage	binary	0/8	2 — fails
expect-full-coverage	dual_rail_steady	7/8	1 — fails

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

[Eulerianial]

I tested the same using tinyalu design. Observed the in-equivalence as reported above.
Adding the design/log here.

tinyalu-formal-run.zip

[ovebryne]

Retested on main @ c7b8fe6d, which adds --learn-internal-relations
(default true). The reproducer is unchanged, and the pass certifies nothing.

arm	candidates	proved	result
default (learning on)	64	0	87.50% (7/8), dout[5]
--learn-internal-relations false	–	–	87.50% (7/8), dout[5] — identical
--allow-x-equality-in-internal-relations false	64	0	87.50% (7/8)
--sec-engine k_induction	64	0	no verdict — killed at 30 min (PDR: ~25 s)
N=4 (an instance that passes)	32	0	proves anyway

From KEPLER_SEC_DIAG=1:

SEC summary: internal_relation_candidates=64 proved_rail_equalities=0 allow_x_equality_in_internal_relations=1

Candidate generation looks right — 64 is exactly the register-bit count (8
accumulators x 8 bits). Certification proves none of them, on a design compared
against itself, where every candidate is true by construction and the
conjunction is inductive in one step.

proved_rail_equalities=0 holds regardless of the X-equality option and
regardless of whether the overall proof succeeds — the N=4 instance proves while
still certifying zero relations. It also holds under k_induction, which emits
the same 64 / 0 summary under KEPLER_SEC_DIAG=1 and then produces no verdict
at all on this case — we killed it at 30 minutes, against ~25 s for PDR on the
identical input. That points at the
certification step rather than at candidate generation or at any one engine.

The k_induction non-termination is a separate observation from the one this
issue is about; say the word and we will file it on its own.

Happy to run any instrumented build against this case.

[nanocoh]

The pin for the PR was a mistake. it was for another issue. For this issue a fix is pending check in and will update when it is done.

[nanocoh]

Hi @ovebryne and @Eulerianial , can you please try again your tests with latest main? we introduced some optimizations to handle better this case in SEC and it should now make your tests pass with full equivalence.

[ovebryne]

Confirmed fixed on main @ c2e6a070. Thank you — the whole family passes now,
not just the reported case.

Same generator as the reproducer, N independent accumulators, default encoding,
--sec-engine pdr:

N	4	5	6	7	8	9	10	12	16	24	32	64
before	ok	ok	ok	6/7	7/8	ok	8/10	11/12	ok	ok	ok (49 s)	–
now	ok	ok	ok	ok	ok	ok	ok	ok	ok	ok	ok (0 s)	ok (3 s)

Every size proves, all in ≤3 s. I added N=64 as a larger check; it also proves.

The certification step is doing the work now:

internal_relation_candidates=64 proved_rail_equalities=128
SEC proved equivalence under the dual-rail steady-state abstraction at k = 1

Previously that read proved_rail_equalities=0, and the run reached only
partially proved … at k = 8. (The two counters look to be in different units —
128 rail-equalities against 64 candidates, presumably two rails per relation —
so read it as "all of them now certify" rather than a mismatch.) Worth noting this is a large speedup as well as a
correctness fix — N=32 went from 49 s to 0 s, and the non-monotonic behaviour
across sizes is gone entirely.

Two arms from my earlier comment are unchanged

Both re-run on the same c2e6a070 build, same design:

arm	result
--sec-encoding binary	0.00% (0/8), every output skipped — dout[0]: design0 depends on reset-unanchored internal state 99.Q[7]
--sec-engine k_induction	no verdict; killed at 300 s (PDR: 0 s on the same input)

Neither is what this issue was filed about, so I am happy for it to be closed on
the strength of the default path. Tell me whether you would like either of those
as its own issue and I will file with a reproducer — they use the same 33-line
design, only a different flag.

[Eulerianial]

Confirm fixed on main @ c2e6a070 for tinyalu design also.
The solver hit all the PO (Primary Outputs) points with k=1 unrolling of time.

It will be also good to add the sequential point information along with the POs in the coverage report (I will make a separate ticket for it).