Two different machines

An immediate assertion is a procedural statement. It runs when the surrounding code reaches it, evaluates its expression instantly with current values, and is done.

A concurrent assertion is a clocked declaration. It samples signals on a clock edge, can span many cycles, and runs for the whole simulation. An immediate assertion cannot say ack within 3 cycles, and a concurrent assertion is overkill for a cast check.

1
2
3
4
5
6
7
8
9

// snippet
// IMMEDIATE: runs when the task executes, sees current values
task drive_burst(input bit is_burst, input int id);
  a_cast: assert (is_burst)
    else $error("item %0d is not a burst item", id);
endtask

// IMMEDIATE: re-evaluates on every input change inside combinational code
// a_onehot: assert ($onehot0(grant)) else $error("grant not one-hot-0");

1
2
3
4
5
6

// snippet
// CONCURRENT: declarative, clocked, temporal
// "every req gets an ack within 1 to 3 cycles"
// ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
//   req |-> ##[1:3] ack)
//   else $error("ack missed the 3-cycle window");

Module, interface or checker scope is the norm for concurrent assertions. A concurrent assertion inside a clocked procedure with an inferred clock is legal but legacy style.

Instant checks and the glitch problem

An immediate assertion in combinational code can fire on a delta-cycle glitch. Inputs may settle in several delta steps within one slot, and the assertion sees the transient combination that no flip-flop would capture.

Deferred variants exist for exactly this. IEEE 1800-2009 added assert #0, and 1800-2012 added assert final. Both evaluate the expression when the statement runs, but defer the report: #0 matures in the Observed region, and final in the Postponed region. If the process runs again before the report matures, the pending report is flushed, so a failure cured by later deltas is never printed.

1
2
3
4
5
6
7
8

// snippet
// plain immediate: may fire on delta-cycle glitches
// a_glitchy: assert (!(ready && error));
// observed deferred: report matures in the Observed region, glitch-immune
// a_observed: assert #0 (!(ready && error))
//   else $error("ready and error both high");
// final deferred: report matures in the Postponed region, on settled values
// a_final: assert final (!(ready && error));

Clocked checks and the ack window

A concurrent assertion pins evaluation to clock ticks, so it can express relations across cycles. The diagram shows one request answered two cycles later, inside a 1-to-3 window.

Watch ack against req. The attempt opened in slot 1 closes in slot 3.

• Slot 0: req 0, ack 0. Idle, and every attempt passes vacuously.

• Slot 1: req 1. An attempt opens; its window is slots 2 to 4.

• Slot 2: req 0, ack 0. Cycle 1 of the window, still waiting.

• Slot 3: ack 1. Answered in cycle 2, so the attempt passes.

• Slot 4: req 0, ack 0. Idle, with nothing in flight.

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

module req_ack_props (
  input logic clk,
  input logic rst_n,
  input logic req,
  input logic ack
);
  ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
    req |-> ##[1:3] ack)
    else $error("ack missed the 3-cycle window");

  // Approximate: some req in the 3 cycles before ack. An exact check
  // needs an outstanding-request counter.
  ap_ack_alone: assert property (@(posedge clk) disable iff (!rst_n)
    ack |-> ($past(req, 1) || $past(req, 2) || $past(req, 3)))
    else $error("ack with no req in the previous 3 cycles");
endmodule

The second assertion matches the 1-to-3 window of the first. Requiring $past(req) alone would fail the waveform above, where ack comes two cycles after req.

Decision rules

Choose by the question, not by habit. Instant value checks belong in procedural code, and anything with time in it needs a clock.

Testbench

The bench runs both kinds for real. An immediate $onehot0 check runs once for each of the 16 grant values. The two concurrent checks above watch an answered request, then a planted unanswered request and a planted ack with no request.

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

module tb_imm_conc;
  logic clk = 0;
  always #5 clk = ~clk;
  logic rst_n = 0;
  logic req = 0, ack = 0;
  logic [3:0] grant;
  int imm_fails = 0, win_fails = 0, alone_fails = 0;

  // Concurrent: clocked, sampled before each edge, spans cycles.
  // A real bench would report with $error; Verilator stops at the first $error,
  // so these benches count failures in the action block and keep running.
  ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
    req |-> ##[1:3] ack) else win_fails++;
  ap_ack_alone: assert property (@(posedge clk) disable iff (!rst_n)
    ack |-> ($past(req, 1) || $past(req, 2) || $past(req, 3))) else alone_fails++;

  // Immediate: runs when the code reaches it, with the values of that moment.
  task automatic check_grant(logic [3:0] g);
    a_onehot0: assert ($onehot0(g)) else imm_fails++;
  endtask

  initial begin
    for (int g = 0; g < 16; g++) check_grant(4'(g));      // 5 of 16 values are one-hot-0
    $display("immediate $onehot0 over all 16 grant values: %0d failures (11 expected)", imm_fails);
    repeat (2) @(negedge clk);
    rst_n = 1;
    @(negedge clk); req = 1;                               // answered 2 cycles later
    @(negedge clk); req = 0;
    @(negedge clk); ack = 1;
    @(negedge clk); ack = 0;
    repeat (3) @(negedge clk);
    $display("answered request: %0d window failures", win_fails);
    @(negedge clk); req = 1;                               // planted bug: never answered
    @(negedge clk); req = 0;
    repeat (5) @(negedge clk);
    @(negedge clk); ack = 1;                               // planted bug: an ack with no request
    @(negedge clk); ack = 0;
    repeat (2) @(negedge clk);
    $display("unanswered request: %0d window failures; lone ack: %0d failures", win_fails, alone_fails);
    if (imm_fails != 11 || win_fails != 1 || alone_fails != 1) $fatal(1, "FAIL: counts %0d %0d %0d", imm_fails, win_fails, alone_fails);
    $display("PASS: the immediate check caught 11 bad grants, and each concurrent check caught its one planted bug");
    $finish;
  end
endmodule

immediate $onehot0 over all 16 grant values: 11 failures (11 expected)
answered request: 0 window failures
unanswered request: 1 window failures; lone ack: 1 failures
PASS: the immediate check caught 11 bad grants, and each concurrent check caught its one planted bug

Related topics

• Sequences

• Implication and properties