Why it matters

Every large sign-off has open proofs: the induction step will not close, the bound will not reach, the solver will not finish. What separates a defensible package from a hopeful one is what happens next. An inconclusive result is a work item with four exits, and a waiver is the last of them, granted only for evidence, never for optimism.

The core idea

The four exits in order: reduce the problem with abstraction, cut points or case splits until the proof closes; extend the bound with a fresh justification; back the obligation with another method, usually simulation with directed tests plus covers; or waive it with evidence. A waiver needs a proven invariant or a reviewed constraint, an owner, an expiry, and the neighbour's agreement where the behaviour crosses a block boundary. The sentence cannot happen is never evidence; the invariant that excludes it, proved, is.

The run below is the honest starting point: the induction step open on the decade counter without its helper, base case passing, step failing. Inconclusive, with the failing step trace pointing at the unreachable states the helper would exclude. Reduction is the right exit here: add the range invariant and the same property proves, so this case needs a proof, not a waiver. The topic on bounded versus unbounded proofs, linked below, explains why the step fails from unreachable states.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

// formal: prove 10 expect unproven slang top mod10_counter define HELPER=0
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
//   rst (synchronous, active high) : count <= 0
//   en  = 1                        : count <= (count == 9) ? 0 : count + 1
//   en  = 0                        : count holds
//   tc  = en && (count == 9)       : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);

  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // P2: count is never 15. True, but NOT inductive on its own: the unreachable states
  // 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever, so no k
  // of k-induction closes it).
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  // P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate

  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end

  // sticky flag: the counter has wrapped at least once
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

Three waiver texts, one acceptable

The cases below are about a different, illustrative block: a retry counter whose induction step stays open because the step can start with the enable active during a reset-synchroniser busy window that the neighbouring block never produces.

Every waiver is a record, and a script can refuse a record that has a hole. The check below rejects a record with a missing field, an empty evidence reference, or an expiry in the past; the dates and names are illustrative.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

# illustrative: a waiver record and the gate that refuses incomplete or expired ones
from datetime import date

FIELDS = ("prop", "evidence", "owner", "expiry", "backup")

def check_waiver(rec, today):
    faults = [f + ": missing" for f in FIELDS if not rec.get(f)]
    if rec.get("expiry") and not faults and date.fromisoformat(rec["expiry"]) < today:
        faults.append("expired: reopen as an open row")
    return faults

today = date(2026, 11, 1)
good = {"prop": "a_retry_hold", "evidence": "neighbour assertion a_no_en_while_busy (proven)",
        "owner": "block owner", "expiry": "2027-01-31", "backup": "tests t_reset_recovery_1, t_reset_recovery_2"}
assert check_waiver(good, today) == []
# the three ways a waiver goes wrong
assert check_waiver(dict(good, evidence=""), today) == ["evidence: missing"]
assert check_waiver(dict(good, owner=None, backup=""), today) == ["owner: missing", "backup: missing"]
assert check_waiver(dict(good, expiry="2026-10-01"), today) == ["expired: reopen as an open row"]
print("PASS: complete waiver accepted; missing evidence, owner, backup and an expired date are each refused")

Expired waivers reopen automatically: a waiver is a loan against future proof, not a pardon.

What the reviewer looks for

• Each inconclusive row names its exit: reduction attempted, deeper bound, backup tests, or waiver with evidence.

• Waivers cite proved invariants or reviewed constraints with the neighbour's proven assertion, never bare assertions about what cannot happen.

• Every waiver has an owner, an expiry, and a backup; expired waivers are open rows again.

Verify and debug

Before writing any waiver, spend the reduction budget: check the cone size and the depth progress first, then abstract, split or strengthen. Most inconclusive results at sign-off time are convergence problems with known cures, and a waiver written before reduction is tried is a confession that the proof was abandoned, not completed. When simulation is the backup, name the exact tests and covers that carry the obligation, and link them in the ledger.

Related topics

• Next: Stale Proofs and Source Hashes

• Formal: Bounded vs Unbounded Proofs