Justifying a Bound

On this page

Part 7 of 10, lesson 9 of 15Formal Coverage and SignoffAll levels

Why it matters

A bounded run reports no failure up to N, and a bug at cycle N plus 1 walks past it untouched. The decade counter's wrap bug is the standing exhibit: bounded to 10 it passes, bounded to 11 it fails, and the difference is one cycle. A bounded result is sign-off grade only with a justification, and this lesson derives the minimum bound for three designs, then runs a bug that needs all of it on each.

The core idea

A bound is justified when an argument shows no bug can hide past it. Three accepted arguments: the sum of reset, trigger and latency, which says every behaviour the property covers starts, unfolds and is checked inside the bound; a diameter or recurrence argument, which says every reachable state is visited inside the bound; or an inductive proof, which removes the bound question. The working rule for the sum form:

N >= r ese t s t e p s + t r i g g er l e n g t h + w or s t - c a se l a t e n cy + 1

The terms: reset steps are the steps spent in reset; trigger length is the number of cycles the stimulus must last; latency is the extra cycles between the end of the stimulus and the cycle the check reads the effect, zero when the check reads state that the last stimulus edge has just updated. The final plus one converts a last step number into a depth, because depth N checks steps 0 to N minus 1. The rule is a lower bound: a bound below it is not a weaker result, it is no result.

Worked example: three designs, three measured edges

Design and bug	Reset	Trigger	Derived minimum	Why the trigger is that long
Decade counter, wraps at 10	1	9	11	Nine enabled cycles take the count to 9, where the terminal pulse is wrong.
Arbiter, pointer stuck (helper invariants off)	1	4	6	Four cycles of full contention make requester 1 wait 4 cycles, one past the limit of 3.
Bridge, skid never captures	1	2	4	Two accepted words: the second arrives while the first is stalled and is dropped.

Every latency is zero because each check reads a register or a counter that the last stimulus edge has just updated. The script derives the three minima and then enforces them: a bound below the derived minimum is rejected, and so is a measured edge that disagrees with the derivation.

example.py

# bound justification worksheet: minimum defensible depth per property
def min_bound(reset, trigger, latency):
    return reset + trigger + latency + 1

def accept(bound, derived):
    # a chosen bound is defended only if it reaches the derived minimum
    return bound >= derived

cnt = min_bound(1, 9, 0)   # counter: reset, nine enabled cycles, pulse read at once
arb = min_bound(1, 4, 0)   # arbiter: reset, four contention cycles, wait counter read at once
brg = min_bound(1, 2, 0)   # bridge: reset, two accepted words, conservation counters read at once
assert (cnt, arb, brg) == (11, 6, 4), (cnt, arb, brg)
# measured edges from the runs below: the last depth that passes and the first that fails
edges = {"counter": (10, 11), "arbiter": (5, 6), "bridge": (3, 4)}
derived = {"counter": cnt, "arbiter": arb, "bridge": brg}
for name, (passes, fails) in edges.items():
    assert fails == derived[name] and passes == derived[name] - 1, name
# the gate: shorter bounds are rejected, the derived one is accepted
assert not accept(10, cnt) and accept(11, cnt)
assert not accept(5, arb) and accept(6, arb)
assert not accept(3, brg) and accept(4, brg)
# the same function on a registered response (illustrative: reset 2, 4 requests, latency 6)
assert min_bound(2, 4, 6) == 13 and not accept(12, min_bound(2, 4, 6))
print("PASS: minima 11, 6 and 4 equal the measured edges; any shorter bound is rejected")

The counter pair, one cycle apart: bounded to 10 the bug is invisible; bounded to 11 it is a counterexample at step 10.

mod10_counter.sv

// formal: bmc 10 expect pass slang top mod10_counter define BUG=1
`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

mod10_counter.sv

// formal: bmc 11 expect fail slang top mod10_counter define BUG=1
`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

The arbiter pair, with the helper invariants off so that the requirement itself is what fails: starvation of requester 1 needs reset, four contention cycles and one more step. With the helpers on, a helper invariant fails earlier, but an invariant failing is not yet the requirement failing: the sign-off bound is derived from the requirement.

rr_arbiter.sv

// formal: bmc 5 expect pass slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
// rr_arbiter: 4-requester round-robin arbiter. Grant is combinational from req and
// the 2-bit pointer `last` (index granted most recently). Search order starts at
// last+1 and wraps. A grant is given in the same cycle a request is seen, and a
// grant lasts one cycle only (no lock). Synchronous active-high reset: last = 3, so
// requester 0 has priority first.
// BUG: 0 none, 1 starvation (pointer not advanced when requester 0 wins),
// 2 double grant (low-priority path ORed in even when a higher-priority request exists),
// 3 grant without request (the last holder is ORed into the low-priority search).
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  reg [1:0] last;

  // requests strictly after `last` in rotation order (higher priority part)
  wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
                       (last == 2'd1) ? 4'b1100 :
                       (last == 2'd2) ? 4'b1000 : 4'b0000;
  wire [3:0] hi_req  = req & hi_mask;
  wire [3:0] lo_req  = (BUG == 3) ? (req | (4'b0001 << last)) : req;

  function [3:0] lowest;           // lowest set bit, one-hot (0 if none)
    input [3:0] v;
    lowest = v & (~v + 4'd1);
  endfunction

  wire [3:0] g_hi = lowest(hi_req);
  wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
  assign grant = g_hi | g_lo;

  wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;

  always @(posedge clk) begin
    if (rst) last <= 2'd3;
    else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
  end

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

  // wt[i]: consecutive cycles requester i has requested without being granted
  reg [2:0] wt0, wt1, wt2, wt3;
  always @(posedge clk) begin
    if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
    else begin
      wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
      wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
      wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
      wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
    end
  end

  always @(*) if (!init) begin
    a_onehot0:  assert ((grant & (grant - 4'd1)) == 4'd0);          // at most one grant
    a_no_phantom: assert ((grant & ~req) == 4'd0);                    // grant implies request
    a_work_cons:  assert (!(|req) || (|grant));                       // some request -> some grant
    // bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
    a_wt0: assert (wt0 <= 3'd3);
    a_wt1: assert (wt1 <= 3'd3);
    a_wt2: assert (wt2 <= 3'd3);
    a_wt3: assert (wt3 <= 3'd3);
  end

  // helper invariants for the induction step of the wait bounds: waited cycles plus the
  // requesters still ahead in rotation order never exceed 3
  function [1:0] ahead;             // how many grants can still precede requester i
    input [1:0] i;
    ahead = i - last - 2'd1;        // 0..3 (mod 4)
  endfunction
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
      h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
      h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
      h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
    end
  end endgenerate

  // covers
  always @(*) if (!init) begin
    c_g0: cover (grant[0]);
    c_g1: cover (grant[1]);
    c_g2: cover (grant[2]);
    c_g3: cover (grant[3]);
    c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
    c_idle: cover (req == 4'b0000 && grant == 4'b0000);
  end
`endif
endmodule

rr_arbiter.sv

// formal: bmc 6 expect fail slang top rr_arbiter define BUG=1 define HELPER=0
`define FORMAL
// rr_arbiter: 4-requester round-robin arbiter. Grant is combinational from req and
// the 2-bit pointer `last` (index granted most recently). Search order starts at
// last+1 and wraps. A grant is given in the same cycle a request is seen, and a
// grant lasts one cycle only (no lock). Synchronous active-high reset: last = 3, so
// requester 0 has priority first.
// BUG: 0 none, 1 starvation (pointer not advanced when requester 0 wins),
// 2 double grant (low-priority path ORed in even when a higher-priority request exists),
// 3 grant without request (the last holder is ORed into the low-priority search).
module rr_arbiter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] req,
  output wire [3:0] grant
);
  reg [1:0] last;

  // requests strictly after `last` in rotation order (higher priority part)
  wire [3:0] hi_mask = (last == 2'd0) ? 4'b1110 :
                       (last == 2'd1) ? 4'b1100 :
                       (last == 2'd2) ? 4'b1000 : 4'b0000;
  wire [3:0] hi_req  = req & hi_mask;
  wire [3:0] lo_req  = (BUG == 3) ? (req | (4'b0001 << last)) : req;

  function [3:0] lowest;           // lowest set bit, one-hot (0 if none)
    input [3:0] v;
    lowest = v & (~v + 4'd1);
  endfunction

  wire [3:0] g_hi = lowest(hi_req);
  wire [3:0] g_lo = lowest(lo_req) & {4{(hi_req == 4'b0) || (BUG == 2)}};
  assign grant = g_hi | g_lo;

  wire [1:0] gidx = grant[0] ? 2'd0 : grant[1] ? 2'd1 : grant[2] ? 2'd2 : 2'd3;

  always @(posedge clk) begin
    if (rst) last <= 2'd3;
    else if (|grant && !(BUG == 1 && grant[0])) last <= gidx;
  end

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

  // wt[i]: consecutive cycles requester i has requested without being granted
  reg [2:0] wt0, wt1, wt2, wt3;
  always @(posedge clk) begin
    if (rst) begin wt0 <= 3'd0; wt1 <= 3'd0; wt2 <= 3'd0; wt3 <= 3'd0; end
    else begin
      wt0 <= (req[0] && !grant[0]) ? wt0 + 3'd1 : 3'd0;
      wt1 <= (req[1] && !grant[1]) ? wt1 + 3'd1 : 3'd0;
      wt2 <= (req[2] && !grant[2]) ? wt2 + 3'd1 : 3'd0;
      wt3 <= (req[3] && !grant[3]) ? wt3 + 3'd1 : 3'd0;
    end
  end

  always @(*) if (!init) begin
    a_onehot0:  assert ((grant & (grant - 4'd1)) == 4'd0);          // at most one grant
    a_no_phantom: assert ((grant & ~req) == 4'd0);                    // grant implies request
    a_work_cons:  assert (!(|req) || (|grant));                       // some request -> some grant
    // bounded response (a starvation-freedom proxy): nobody waits more than 3 cycles
    a_wt0: assert (wt0 <= 3'd3);
    a_wt1: assert (wt1 <= 3'd3);
    a_wt2: assert (wt2 <= 3'd3);
    a_wt3: assert (wt3 <= 3'd3);
  end

  // helper invariants for the induction step of the wait bounds: waited cycles plus the
  // requesters still ahead in rotation order never exceed 3
  function [1:0] ahead;             // how many grants can still precede requester i
    input [1:0] i;
    ahead = i - last - 2'd1;        // 0..3 (mod 4)
  endfunction
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      h_wt0: assert (wt0 + {1'b0, ahead(2'd0)} <= 3'd3);
      h_wt1: assert (wt1 + {1'b0, ahead(2'd1)} <= 3'd3);
      h_wt2: assert (wt2 + {1'b0, ahead(2'd2)} <= 3'd3);
      h_wt3: assert (wt3 + {1'b0, ahead(2'd3)} <= 3'd3);
    end
  end endgenerate

  // covers
  always @(*) if (!init) begin
    c_g0: cover (grant[0]);
    c_g1: cover (grant[1]);
    c_g2: cover (grant[2]);
    c_g3: cover (grant[3]);
    c_contend: cover (req == 4'b1111 && wt3 == 3'd3);
    c_idle: cover (req == 4'b0000 && grant == 4'b0000);
  end
`endif
endmodule

The bridge pair: the conservation check fails at step 3, when the second accepted word is dropped, so depth 3 passes and depth 4 fails.

hs_bridge.sv

// formal: bmc 3 expect pass slang top hs_bridge define BUG=1
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;

  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;

  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;

  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      // output holds; a new input is parked in the skid register
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      // output empty or consumed this cycle
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end

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

  // ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
  reg [3:0] acc, dlv;
  always @(posedge clk) begin
    if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
    else begin
      if (in_xfer)  acc <= acc + 4'd1;
      if (out_xfer) dlv <= dlv + 4'd1;
    end
  end

  always @(*) if (!init) begin
    a_skid_needs_out: assert (!svld || ovld);                       // skid only used behind a full output
    a_conserve:       assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
  end

  // ---- protocol: a stalled output must hold valid and data ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
    a_data_hold:  assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
    // ready is a registered function: it cannot depend on out_ready in the same cycle
    a_no_ready_comb: assert (in_ready == !svld);
  end

  // ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
  // free constant (see the FIFO module): anyconst wire plus an equal-to-its-old-copy assumption
  (* anyconst *) wire [3:0] tn;
  reg [3:0] tn_q;
  always @(posedge clk) tn_q <= tn;
  always @(*) if (!init) assume (tn == tn_q);
  reg       tv;      // the tracked word has been accepted and not yet delivered
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
      else if (out_xfer && dlv == tn) tv <= 1'b0;
    end
  end
  always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      // where the tracked word lives: output stage if it is next to leave, else skid
      h_in_out:  assert (!(tv && dlv == tn) || (ovld && odat == td));
      h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
      h_pos:     assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
    end
  end endgenerate

  // ---- covers ----
  always @(*) if (!init) begin
    c_stall:     cover (stalled);
    c_skid_used: cover (svld);
    c_backpress_full: cover (!in_ready);
    c_flow:      cover (in_xfer && out_xfer);
  end
`endif
endmodule

hs_bridge.sv

// formal: bmc 4 expect fail slang top hs_bridge define BUG=1
`define FORMAL
// hs_bridge: valid/ready register stage with a skid buffer (2-entry elastic stage).
// Output stage `ovld/odat` plus skid `svld/sdat`. in_ready = !svld, so it depends on a
// register only (no combinational path from out_ready to in_ready). Synchronous
// active-high reset empties both stages. A transfer happens on a cycle where valid
// and ready are both 1.
// BUG: 0 none, 1 data dropped on stall (skid never captures), 2 valid dropped
// (stalled output loses valid when the input idles), 3 data changes under backpressure
// (stalled output overwritten by new input).
module hs_bridge #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  output wire       in_ready,
  input  wire [7:0] in_data,
  output wire       out_valid,
  input  wire       out_ready,
  output wire [7:0] out_data
);
  reg       ovld, svld;
  reg [7:0] odat, sdat;

  assign in_ready  = !svld;
  assign out_valid = ovld;
  assign out_data  = odat;

  wire in_xfer  = in_valid && in_ready;
  wire out_xfer = ovld && out_ready;
  wire stalled  = ovld && !out_ready;

  always @(posedge clk) begin
    if (rst) begin
      ovld <= 1'b0;
      svld <= 1'b0;
    end else if (stalled) begin
      // output holds; a new input is parked in the skid register
      if (in_xfer && BUG != 1) begin svld <= 1'b1; sdat <= in_data; end
      if (BUG == 2 && !in_valid) ovld <= 1'b0;
      if (BUG == 3 && in_xfer)   odat <= in_data;
    end else begin
      // output empty or consumed this cycle
      if (svld) begin
        odat <= sdat; ovld <= 1'b1; svld <= 1'b0;
      end else begin
        odat <= in_data; ovld <= in_valid;
      end
    end
  end

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

  // ---- conservation: accepted - delivered = items held (counters wrap at 16) ----
  reg [3:0] acc, dlv;
  always @(posedge clk) begin
    if (rst) begin acc <= 4'd0; dlv <= 4'd0; end
    else begin
      if (in_xfer)  acc <= acc + 4'd1;
      if (out_xfer) dlv <= dlv + 4'd1;
    end
  end

  always @(*) if (!init) begin
    a_skid_needs_out: assert (!svld || ovld);                       // skid only used behind a full output
    a_conserve:       assert (acc - dlv == {3'b0, ovld} + {3'b0, svld});
  end

  // ---- protocol: a stalled output must hold valid and data ----
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_valid_hold: assert (!($past(out_valid) && !$past(out_ready)) || out_valid);
    a_data_hold:  assert (!($past(out_valid) && !$past(out_ready)) || out_data == $past(out_data));
    // ready is a registered function: it cannot depend on out_ready in the same cycle
    a_no_ready_comb: assert (in_ready == !svld);
  end

  // ---- data integrity by tracked-item abstraction: follow the n-th accepted word ----
  // free constant (see the FIFO module): anyconst wire plus an equal-to-its-old-copy assumption
  (* anyconst *) wire [3:0] tn;
  reg [3:0] tn_q;
  always @(posedge clk) tn_q <= tn;
  always @(*) if (!init) assume (tn == tn_q);
  reg       tv;      // the tracked word has been accepted and not yet delivered
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (in_xfer && acc == tn) begin tv <= 1'b1; td <= in_data; end
      else if (out_xfer && dlv == tn) tv <= 1'b0;
    end
  end
  always @(*) if (!init && out_xfer && tv && dlv == tn) a_data: assert (out_data == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) begin
      // where the tracked word lives: output stage if it is next to leave, else skid
      h_in_out:  assert (!(tv && dlv == tn) || (ovld && odat == td));
      h_in_skid: assert (!(tv && dlv + 4'd1 == tn) || (svld && sdat == td));
      h_pos:     assert (!tv || (dlv == tn) || (dlv + 4'd1 == tn));
    end
  end endgenerate

  // ---- covers ----
  always @(*) if (!init) begin
    c_stall:     cover (stalled);
    c_skid_used: cover (svld);
    c_backpress_full: cover (!in_ready);
    c_flow:      cover (in_xfer && out_xfer);
  end
`endif
endmodule

In all three the derived minimum equals the measured edge, which is what a combinational response looks like. When the response is registered after a long pipeline, the derived minimum can exceed the first failing depth by one, because the formula assumes the full latency still has to elapse after the stimulus. That is safe: the formula is a lower bound for defending a bound, and a bound above the true edge is merely generous. The checkYourself below uses such a case.

What the reviewer looks for

Every bounded row cites one of the three arguments with its numbers: reset steps, trigger length, latency, plus one.
The derived minimum is recomputed when the design changes; the bound never survives a latency change unreviewed.
A bug variant exists that needs the full depth, proving the bound is load-bearing rather than round.

Verify and debug

Stress the bound, not just the design: rerun each bounded proof one depth short of its derived minimum and confirm the bug variant passes there, then ask what would hide in the missing cycles. If a deeper bug class exists past the bound, the justification must exclude it explicitly, for example with a diameter argument, or the bound moves. Pointer wraps are the classic miss: a FIFO overflow needs the fill depth, but a wrap-around bug needs about twice the operations, and the bound must cover the larger.

Check yourself A pipeline answers in 6 cycles, reset lasts 2, and a bug needs 4 back-to-back requests. What is the minimum bound?

Reset 2, plus 4 requests, plus latency 6, plus 1: 13 (illustrative numbers). Any bound below 13 cannot defend the check. Whether the bug first fails at 13 or one earlier depends on exactly when the response appears, which is why the sum is a lower bound for the defence and not a prediction of the first failing depth.

Navigate

Why it matters

The core idea

Worked example: three designs, three measured edges

What the reviewer looks for

Verify and debug

Related topics

Justifying a Bound

Why it matters

The core idea

Worked example: three designs, three measured edges

What the reviewer looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: three designs, three measured edges

What the reviewer looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: three designs, three measured edges

What the reviewer looks for

Verify and debug

Related topics

Up next