Immediate and concurrent

An immediate assertion is a procedural statement, assert (expr) inside an always block, task, or function. It evaluates instantly with current, possibly mid-timestep values, like an if statement that errors.

A concurrent assertion is declarative: assert property (@(posedge clk) ...). It evaluates on clock edges using sampled values and can describe multi-cycle temporal behavior.

This fragment is an illustration, so the course checks skip it; the bench at the end of the page runs the same ideas.

1
2
3
4
5
6
7
8

// snippet
// Immediate: procedural, instant, current values
// a_imm: assert (onehot_grant) else $error("grant not onehot");

// Concurrent: declarative, clocked, sampled values, temporal
a_con: assert property (
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:4] ack);

Immediate assertions can sit anywhere procedural code runs, including classes and testbench components, which is why assert (obj.randomize()) is an immediate assertion. They are vulnerable to glitches and ordering races because they fire mid-timestep.

Concurrent assertions live at module, interface, program or checker scope, or inside always and initial blocks (procedural concurrent assertions), but never in classes. They are race-free by construction, because they read sampled values. The sampling model, not the syntax, is the real difference.

Sampling and attempts

A concurrent assertion samples in the Preponed region of the timestep: the values just before the clock edge, ahead of any updates from that edge. Evaluation happens later in the same timestep, in the Observed region, and action blocks run after that.

The region order is Preponed, then Active with its NBA subregion where flops update, then Observed, then Reactive for testbench code, then Postponed where settled values can be printed. An assertion never sees the new value a flop takes on the same edge: it sees the old one, exactly what a real flop would capture.

The simulator starts a new evaluation attempt at every sampling edge. Each attempt checks the antecedent with that edge's sampled values and exits vacuously on a non-match. On a match it spawns a consequent obligation that may run for many cycles, so several attempts of one assertion can be alive at once.

Three practical consequences follow. Level antecedents on held signals multiply live attempts into a retrigger storm. Local variables are per attempt, which is why tag matching works and shared counting does not. Each attempt passes or fails independently.

Roles and names

Assert, assume, and cover share syntax and differ only in obligation. Assert says the design must satisfy the property. Assume says the environment is promised to satisfy it: in formal the tool only explores stimulus where it holds, and in simulation most tools check it like an assert.

Cover records whether the scenario ever occurred. Green needs both sides: an assert with an unexercised antecedent is vacuously green, and a hit cover with no assert is observation without checking.

This fragment is an illustration, so the course checks skip it; the bench at the end of the page runs the same ideas.

1
2
3
4

// snippet
a_ack_pulse: assert property (@(posedge clk) $rose(ack) |=> !ack);
m_req_legal: assume property (@(posedge clk) $rose(req) |=> !req);
c_req_gap1:  cover property (@(posedge clk) req ##2 req);   // two pulses, one idle cycle apart

A wrong assume in formal yields false proofs: the tool prunes legal stimulus, the assert proves over the remainder, and contradictory assumes prove everything vacuously. The senior habit is cover-checking the assumes, proving interesting stimulus still exists under them.

Label every assertion. The label becomes the hierarchical name used by logs, triage scripts, waveform tracks, $assertoff control, formal tables, and plan mapping. Tool-generated names drift across edits and break waivers silently. Designers write white-box invariants at the cause, DV writes black-box protocol checks at the contract, and bind files carry the protocol checks without touching RTL.

Common mistakes

Testbench

The bench checks each answer on Verilator: the overlapping attempts from the table, then an unanswered request, an assume broken by a two-cycle request, a double grant caught by an immediate check, and a cover that counts the two-pulse pattern.

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

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

  // Concurrent: an attempt at every edge; overlapping requests overlap attempts.
  a_con: assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |-> ##[1:4] ack) else win_fails++;
  // assume is checked in simulation exactly like assert.
  m_req_legal: assume property (@(posedge clk) disable iff (!rst_n)
    $rose(req) |=> !req) else assume_fails++;
  c_req_gap1: cover property (@(posedge clk) req ##2 req) gaps++;
  // Immediate: procedural, instant, current values.
  always @(posedge clk) if (rst_n) a_imm: assert ($onehot0(grant)) else imm_fails++;

  initial begin
    repeat (2) @(negedge clk);
    rst_n = 1;
    // The trace from the diagram: req at cycles 1 and 3, one ack at 4.
    @(negedge clk) req = 1; @(negedge clk) req = 0;
    @(negedge clk) req = 1; @(negedge clk) req = 0; ack = 1;
    @(negedge clk) ack = 0;
    repeat (6) @(negedge clk);
    $display("two overlapping requests, one ack inside both windows: %0d failures", win_fails);
    // The second request never answered.
    @(negedge clk) req = 1; @(negedge clk) req = 0; ack = 1; @(negedge clk) ack = 0;
    @(negedge clk) req = 1; @(negedge clk) req = 0;
    repeat (6) @(negedge clk);
    $display("second request unanswered: %0d failure", win_fails);
    @(negedge clk) req = 1; repeat (2) @(negedge clk); req = 0; ack = 1;   // a 2-cycle req breaks the assume
    @(negedge clk) ack = 0;
    repeat (2) @(negedge clk);
    @(negedge clk) grant = 4'b0110; @(negedge clk) grant = 0;      // two grants: the immediate check fires
    repeat (2) @(negedge clk);
    $display("assume broken by a 2-cycle req: %0d; immediate one-hot check: %0d; cover req ##2 req hit %0d times",
             assume_fails, imm_fails, gaps);
    if (win_fails != 1 || assume_fails != 1 || imm_fails != 1 || gaps == 0) $fatal(1, "FAIL: %0d %0d %0d %0d", win_fails, assume_fails, imm_fails, gaps);
    $display("PASS: overlapping attempts passed on their own, and assert, assume, cover and the immediate check each did their job");
    $finish;
  end
endmodule

two overlapping requests, one ack inside both windows: 0 failures
second request unanswered: 1 failure
assume broken by a 2-cycle req: 1; immediate one-hot check: 1; cover req ##2 req hit 1 times
PASS: overlapping attempts passed on their own, and assert, assume, cover and the immediate check each did their job

Related topics

• Handshake Drills

• Q&A: Operators & Semantics