Where assertion time goes

A concurrent assertion starts a new attempt every clock edge. Each attempt can fork threads at every range and branch, and the simulator pays for live threads.

Cost is roughly attempts past the antecedent, times threads per attempt, times thread lifetime. Weak antecedents and unbounded windows dominate all three factors.

• Strengthen antecedents: $rose(start), not 1'b1 or a level held through the burst.

• Bound every range with a real protocol bound, never ##[1:$].

• Use first_match where any single match suffices; fewer threads survive.

• Prefer one assertion with a precise trigger over a cycle-invariant form recomputed each edge.

Bounded liveness

Unbounded threads never die while unresolved. If a buggy design drops responses, each lost response leaks a permanent live thread, the run slows progressively, and the failure reports at end of simulation, far from the cause.

In simulation, replace liveness with bounded liveness. The listing below is not run in this course's checks: it is a fragment, and Verilator 5.048 does not support s_eventually. The testbench proves the bounded form instead.

1
2
3
4
5
6
7
8
9
10
11
12

// not-run: fragment without a module; Verilator 5.048 does not support s_eventually
// LEAKY: one thread per lost response lives until end of sim,
// and the failure only reports at sim end
ap_done_leaky: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(start) |-> s_eventually done);

// BOUNDED: worst-case-plus-margin from the spec; fails AT the
// timeout, near the cause, and the thread always terminates
localparam int MAX_LAT = 200;
ap_done: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(start) |-> ##[1:MAX_LAT] done)
  else $error("done timeout: more than 200 cycles after start");

A generous but finite window is both faster and a better bug report. Reserve unbounded liveness for formal tools, behind a parameter.

Phase control and severity

During reset and reconfiguration, rules are legitimately violated. Scoped controls silence exactly those phases, and re-enable after settle.

The listing below is a fragment that names a tb.dut hierarchy, so it is not run in this course's checks. $assertoff at time zero is enough because nothing is in flight yet. Around a mid-run reset use $assertkill, which aborts in-flight attempts and then stays off until $asserton.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

// not-run: fragment; tb.dut, tb.rst_n and program_registers are not defined here
initial begin
  $assertoff(0, tb.dut);                // X-soup phase: total silence
  wait (tb.rst_n);
  repeat (2) @(posedge tb.clk);
  $asserton(0, tb.dut);                 // main phase: everything on
end

task automatic reconfigure_link();
  $assertoff(0, tb.dut.u_link);         // rules legitimately violated
  program_registers();                  // during reconfig
  @(posedge tb.clk);
  $asserton(0, tb.dut.u_link);
endtask

Severity is routing information for the regression script. The wrong level misroutes triage.

Cap repeated failures but keep the count. One broken wire firing every cycle must not bury the second, different bug sitting a thousand lines lower in the log.

Testbench

A source with six-cycle latency and a freeze input. Phase A arrives on time, phase B freezes fourteen edges, phase C moves data under backpressure twelve times.

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

module latency_src #(
  parameter int LAT = 6
) (
  input logic clk, rst_n,
  input logic start, block_ack,
  output logic done
);
  localparam logic [3:0] LAT_CNT = LAT;
  logic [3:0] cnt;
  logic busy;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cnt <= '0;
      busy <= 1'b0;
      done <= 1'b0;
    end else begin
      done <= 1'b0;
      if (start && !busy) begin
        busy <= 1'b1;
        cnt <= LAT_CNT;
      end else if (busy && !block_ack) begin
        if (cnt == 4'd1) begin
          busy <= 1'b0;
          done <= 1'b1;
        end else begin
          cnt <= cnt - 4'd1;
        end
      end
    end
  end
endmodule

caught done timeout at 235000
caught data moved under backpressure, occurrence 1
caught data moved under backpressure, occurrence 2
caught data moved under backpressure, occurrence 3
PASS: timeout fired at +10, a 1'b1 antecedent would start 14 attempts, noise capped at 3 of 12

Related topics

• When Passing Is the Bug