Attempt start and fail time

A concurrent assertion failure carries two times. The attempt start time is the edge where the attempt began, usually where the antecedent matched.

The fail time is the edge where the consequent became impossible. The protocol violation sits somewhere inside that window.

The message above is a schematic illustration, not a verbatim tool format. Neither Icarus nor Verilator prints attempt-start time or the offending term; commercial thread viewers do.

With an attempt starting every cycle, several attempts are mid-flight at once. Attribute the failure to its own attempt before theorizing.

The waveform off-by-one

Assertions sample in the Preponed region: the value a signal held just before the clock edge. A waveform cursor parked on the edge shows the value after updates instead.

When a signal changes at edge N, the assertion at edge N still saw the old value. The assertion looks one cycle behind the waveform, and it is the cursor placement that is wrong.

The window lane marks the live attempt. Ack arrives after the window closes, so the attempt fails.

• Slot 0: idle; req 0, ack 0, window 0.

• Slot 1: req rises; the attempt starts and the window opens.

• Slot 2: ack still 0; the ##1 thread dies.

• Slot 3: ack still 0; the ##2 thread dies.

• Slot 4: ack still 0; the ##3 thread dies.

• Slot 5: ack still 0; the ##4 thread dies, the window closes, FAIL.

• Slot 6: ack finally rises, one cycle outside the window. The bug is the unanswered request at slot 1.

1. Take attempt start time and fail time from the message; load only that window.

2. Read every signal just before each clock edge; that is what the assertion used.

3. Identify which boolean term broke; binary-search the property terms if the tool does not name it.

4. Decide RTL bug versus assertion bug: wrong window, missing qualifier, or bad reset gating are the usual assertion bugs.

Action blocks that print the truth

An action block runs after the design updates for that edge. Printing a signal directly shows the post-edge value, not the value the assertion tested.

$sampled returns the preponed value, so the message matches the assertion view. $sampled takes only the expression; its clock is inferred from the assertion.

1
2
3
4

// bad-example: prints post-edge values, contradicting the failure
ap_gnt_bad: assert property (@(posedge clk) disable iff (!rst_n)
  req |-> gnt)
  else $error("req=%b gnt=%b", req, gnt);   // may print gnt=1 on a fail

1
2
3
4
5

// snippet: prints what the assertion actually sampled
ap_gnt: assert property (@(posedge clk) disable iff (!rst_n)
  req |-> gnt)
  else $error("[%0t] saw req=%b gnt=%b (sampled)",
              $time, $sampled(req), $sampled(gnt));

Invest in action blocks while writing the assertion, not during the debug. A message with every relevant sampled value plus the time often closes the bug without opening a viewer.

Testbench

A request-to-ack pipeline with a stall input, plus the assertion with a sampled message. Phase A is healthy and fires nothing; phase B stalls through the whole window and fires exactly once.

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

module ack_gen (
  input logic clk, rst_n,
  input logic req, stall,
  output logic ack
);
  logic [2:0] sr;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      sr <= '0;
      ack <= 1'b0;
    end else begin
      sr <= {sr[1:0], (req && !stall)};
      ack <= sr[2];
    end
  end
endmodule

caught late ack at 145000: sampled req=0 ack=0
PASS: healthy ack arrived at +4 and the stalled window stayed quiet

Related topics

• When Passing Is the Bug