Assertions and protocol checks

Two kinds of assertion

An assertion states a condition that must hold and reports when it does not. SystemVerilog has two kinds, and a testbench uses both.

An immediate assertion is a statement in procedural code, such as assert (exp_q.size() > 0) else $error(...);. It checks its condition once, at the moment the statement runs, like an if with a built-in failure report.

A concurrent assertion runs on its own, beside the design, and is checked at every clock edge. It can describe behaviour over several cycles, such as "if an offer is stalled at this edge, it must still be there at the next one".

An immediate assertion in the scoreboard

Immediate assertions suit checks that belong to a particular moment in testbench code. At each transfer, the scoreboard can assert that an expectation is waiting, which catches a response that nobody asked for.

The else part is the action block. It runs only on failure, and it should print the time and the values that matter, as Module 1 recommends for every message. A label, as in have_exp: assert ..., names the assertion in reports.

A concurrent assertion for the handshake

The source's rule from lesson 6.5 becomes one property: (rvalid && !rready) |=> (rvalid && $stable(rdata)). Each part has a precise meaning.

|-> would check the consequent at the same edge as the trigger; |=> checks it one edge later, which is what the rule needs. At edges where the trigger is false, the property passes without checking anything.

Sampled values, again

A concurrent assertion reads every signal in the Preponed region, the same pre-edge values a #1step clocking block samples. It evaluates in the Observed region, after the design has settled, so it never races the DUT.

$stable(rdata) compares the sampled value at this edge with the sampled value at the previous edge. Related functions such as $past, $rose and $fell work the same way, on sampled values.

Make sure it can fail

An assertion that never fails might be correct, or it might be checking nothing. Run it once against stimulus that breaks the rule on purpose, as the example does, and confirm that it reports the right edge.

assert property (@(posedge clk)
  (rvalid && !rready) |=> rvalid);

assert property (@(posedge clk)
  disable iff (!rst_n)
  (rvalid && !rready) |=> (rvalid && $stable(rdata)));

Also make sure the trigger happens at all. A property whose antecedent is never true passes on every edge; a counter or a cover statement shows whether stalls really occurred.

Reading a failure report

A concurrent assertion reports its failure at the edge where the consequent was false, which for |=> is one edge after the trigger. Look one cycle earlier in the waveform to find the stalled offer that started the check.

Values printed in the action block are the current values, which may already have moved on. Print $sampled(rdata) to show the value the assertion actually used.

Choosing between the two kinds

Use an immediate assertion for a condition that belongs to one moment in procedural code, such as a scoreboard lookup or a configuration check. It costs nothing between the times its statement runs.

Use a concurrent assertion for a rule about signals over clock cycles, such as a handshake. It runs on every edge, whether or not any testbench code is looking, which is exactly what makes it catch problems early.

Where to go next

This lesson used one property and two operators. The Assertions track covers sequences, the full set of operators, sampled-value functions, local variables and checkers in depth.

Keep protocol assertions in the interface or a bound checker module, next to the signals they watch, so that every test using the interface gets them without extra work.

Try it

The first beat was held through its stalls and passed. The second changed rdata twice while stalled, and hold_offer reported each change at the next rising edge. The third beat arrived with no expectation queued, so the immediate assertion reported it.

Change the property's |=> to |-> and predict which failures still appear, and when.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;
  logic v = 0, r = 0;
  logic [7:0] d = 0;
  a: assert property (@(posedge clk) (v && !r) |=> (v && $stable(d)))
    else $display("fail at %0t", $time);
  initial begin
    @(negedge clk); v = 1; d = 8'h05;
    @(negedge clk);
    @(negedge clk); d = 8'h06;
    @(negedge clk); r = 1;
    @(negedge clk); v = 0; r = 0;
    #20 $finish;
  end
endmodule

(rvalid && !rready) |-> ##1 (rvalid && $stable(rdata))

(rvalid && !rready) |=> rvalid

(rvalid && !rready) |=> (rvalid && rdata == $past(rdata))

(rvalid && !rready) |=> (rvalid && $stable(rdata))

Practice

• Hold the offer Verify · Easy
• Count the beats Verify · Medium