Assertions in procedures, sequences as events

An assertion inside the decode

A concurrent assertion can sit inside an always or initial procedure. It is still a concurrent assertion: it samples values at the clock edge and reports like any other. What changes is when attempts start. An attempt starts only at the edges where the procedure's flow reaches the statement.

always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) state <= IDLE;
  else case (state)
    IDLE: if (start) state <= BUSY;
    BUSY: begin
      one_grant: assert property ($onehot({gnt_a, gnt_b}));
      if (last) state <= IDLE;
    end
  endcase

The rule now follows the RTL's decode. A new busy state that reaches this branch is checked without anyone editing the assertion. The statement does not block the procedure either: it starts an attempt, and the block carries on with its own assignments at once.

The reset branch is part of the path as well. While rst_n is low, the procedure takes the reset branch and never reaches the assertion, so this one-edge rule needs no disable iff. The module-level copy below has to say disable iff (!rst_n) itself.

Where the clock comes from

A procedural assertion with no clock of its own takes one from the procedure's event control. always @(posedge clk) gives @(posedge clk). In the block above, rst_n is also read in the body, so it cannot be the clock, and the clock is posedge clk again.

The inference needs exactly one edge event that the body does not otherwise use. A sensitivity list without an edge, such as @(clk), gives no clock, and so do two candidate edges that the body never reads. Write @(posedge clk) inside the assertion then.

Sampled-value functions in procedural code use the same inferred clock. if ($rose(start)) compares the sampled values of two edges and counts each rise once, while if (start) counts every edge where the level is high. The first quiz question measures both.

Same rule, two places

BUSY: begin
  one_grant: assert property
    ($onehot({gnt_a, gnt_b}));
  ...

one_grant_m: assert property (
  @(posedge clk) disable iff (!rst_n)
  state == BUSY |-> $onehot({gnt_a, gnt_b}));

The example runs both on the same traffic, and they report the same failure. The choice is about what the rule describes. A rule about one branch of this implementation belongs next to that branch. A rule about the interface, which any implementation must obey, belongs at module level or in a bound checker, where an RTL rewrite cannot change what it checks.

Procedural placement has a cost as well. The rule now lives in the RTL file, where the RTL designer reviews, edits and sometimes deletes it, so agree with the design team on which rules live where.

Sequences as events

SVA can also drive procedural code. A named sequence with its own clock can be an event: always @(s_ab) wakes at every end point of s_ab, once per edge where a match completes.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic a = 0, b = 0;
  sequence s_ab; @(posedge clk) a ##2 b; endsequence

  b_two_later: assert property (@(posedge clk) a |-> ##2 b);
  always @(s_ab) $display("s_ab ended at %0t", $time);

  initial begin
    @(negedge clk); a = 1;              // a at 15 and 25
    @(negedge clk);
    @(negedge clk); a = 0; b = 1;       // b at 35 and 45
    @(negedge clk);
    @(negedge clk); b = 0;
    @(negedge clk); a = 1;              // a at 75
    @(negedge clk); a = 0;              // no b at 85
    @(negedge clk);
    @(negedge clk);
    $finish;
  end
endmodule

The wake-up comes at the edge where a match ends, so the block runs once per completed pattern, however many edges the pattern spans.

In a testbench this turns a protocol pattern into a trigger. Count completed handshakes, sample coverage when a burst ends, or hold a stimulus thread until the DUT has finished one, with @(s_done); in an initial block. Keep these sequences fixed-length here.

Assertions can wake procedures from their action blocks too. else -> gnt_late; triggers a named event, and always @(gnt_late) can count it, print the state around it, or stop the stimulus.

Procedural assertions in loops, .triggered, and wait on a sequence are not covered yet.

Try it

Both forms failed only at 55, where both grants were high in BUSY. At 85 both were high again, but the machine was in IDLE: the procedure never reached the assertion, and the module-level antecedent was false.

Delete if (last) state <= IDLE; so the machine stays busy, and predict both lines.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic start = 0;
  int rises, highs;
  always @(posedge clk) begin
    if ($rose(start)) rises++;           // sampled values, clock inferred from the block
    if (start) highs++;
  end
  initial begin
    @(negedge clk); start = 1;           // high at 15, 25, 35
    repeat (3) @(negedge clk);
    start = 0;
    @(negedge clk); start = 1;           // high at 55
    @(negedge clk); start = 0;
    @(negedge clk);
    $display("rises=%0d highs=%0d", rises, highs);
    $finish;
  end
endmodule

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic a = 0, b = 0;
  int ends;
  sequence s_ab; @(posedge clk) a ##1 b; endsequence
  always @(s_ab) ends++;
  initial begin
    @(negedge clk); a = 1;               // a at 15, 25, 35
    @(negedge clk); b = 1;               // b at 25, 35, 45
    @(negedge clk);
    @(negedge clk); a = 0;
    @(negedge clk); b = 0;
    @(negedge clk);
    $display("ends=%0d", ends);
    $finish;
  end
endmodule

case (state) BUSY: a: assert property ($onehot({ga, gb})) else fails++; default: ; endcase

a: assert property ($onehot({ga, gb})) else fails++;

a: assert property (state != BUSY || $onehot({ga, gb})) else fails++;

if (state == BUSY) a: assert property ($onehot({ga, gb})) else fails++;