One moment or many cycles

Use immediate assertions for single-time procedural checks. Use concurrent assertions for clocked temporal behavior across cycles.

The two forms differ in when they evaluate and where they live.

Operator cheat sheet

Concurrent properties are built from a handful of operators. Each one is evaluated at a clock edge on the values sampled there.

The request window

The property below says every request is answered within one to three cycles. The |-> opens the window when req holds, and ##[1:3] accepts a grant on any of the next three edges.

// snippet
assert property (@(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] grant);

The request at slot 2 is answered at slot 6, outside the three-cycle window. The property fails at slot 5.

• Slot 1: idle, req 0 and grant 0.

• Slot 2: req rises, and the window starts.

• Slot 3: one cycle on, grant still 0.

• Slot 4: two cycles on, grant still 0.

• Slot 5: three cycles on, grant still 0, so the window expires here.

• Slot 6: grant finally rises, four cycles after the request, one cycle too late.

• Slot 7: both low again.

The procedural monitor below models this window for known 0/1 inputs, reset asserted across sampling edges, and reset release/input changes on falling edges. Concurrent SVA samples pre-edge values (Preponed); the monitor reads the same stable inputs before NBA updates. Its violation register is observed after NBA with #1. This is a scoped digital equivalence, not a claim about X semantics or every simulator's SVA support.

The combinational grant becomes high after k+1 but is sampled high at k+2. Counting it after NBA at k+1 would label the response one cycle too early. Sample grants before updates; observe registered violation flags after updates.

Common mistakes

1
2
3
4
5

// snippet
always_comb begin
  assert (!(req && grant))
    else $error("req and grant both high");
end

Testbench

The window monitor, a two-cycle responder inside the window, a four-cycle responder outside it, and the testbench. It runs 200 request pulses against each responder.

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

// A responder with latency D: grant is high exactly D cycles after a req
// pulse, as sampled on the clock.
module grant_resp #(parameter [2:0] D = 2) (
  input  logic clk, rst_n, req,
  output logic grant
);
  logic [2:0] cnt;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) cnt <= 3'd0;
    else if (req) cnt <= D;
    else if (cnt != 3'd0) cnt <= cnt - 3'd1;
  end
  assign grant = (cnt == 3'd1);
endmodule

// Plain-RTL form of: req |-> ##[1:3] grant.
// Each pending bit records one request age; overlapping windows are preserved.
module grant_window_mon (
  input  logic clk, rst_n, req, grant,
  output logic violation
);
  logic [2:0] pending;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin pending <= 3'd0; violation <= 1'b0; end
    else begin
      violation <= pending[2] && (grant !== 1'b1);
      if (grant === 1'b1) pending <= {2'b00, req};
      else               pending <= {pending[1:0], req};
    end
  end
endmodule

• Expected for 200 pulses against the two-cycle responder: 200 sampled grants and no violations.

• Expected for the same 200 pulses against the four-cycle responder: 200 violations, one per pulse.

• Directed overlap checks: held requests still expire, and a same-edge grant does not satisfy a newly opened window.

Related topics

• assert, cover, and assume roles

• Common RTL property templates

• SVA cheat sheet and bug hunt