Why assertions

An assertion is a spec sentence that runs

An assertion states a condition the design must meet and reports every time it does not. Written well, it reads like the sentence in the spec it came from, and it checks that sentence on every relevant clock edge of every test.

A scoreboard checks that the right data arrived. Assertions check how it arrived: the protocol rules at each edge. A test needs both, because traffic can carry the right data in a way the spec forbids.

Immediate assertions

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

Immediate assertions suit checks that belong to one moment in testbench code: a scoreboard lookup, a configuration value, a function argument. They know nothing about clock edges or about the cycles before and after.

The standard also has deferred forms, assert #0 and assert final, meant for combinational checks whose inputs settle during a time step. They are not covered yet.

Concurrent assertions

A concurrent assertion runs on its own, beside the design. hold_valid: assert property (@(posedge clk) rvalid && !rready |=> rvalid); is checked at every rising edge of clk, for the whole simulation, whether or not any testbench code is looking.

Concurrent assertions can describe behaviour across clock cycles, which is what most protocol rules are about. They read every signal from just before the edge, so they never race the design; the next lesson shows exactly how.

Each assertion has a label, such as hold_valid, that names it in every report. Choose labels that say the rule, because a failure report is often the first thing someone reads about a bug.

Action blocks and severity

After the property comes an optional pass action and, after else, a fail action. The fail action usually calls a severity task: $error for a broken rule, $fatal when continuing makes no sense, $warning or $info for softer notes.

Without a fail action, a failing assertion calls $error with a message of the simulator's own wording. Writing your own message with the time and the values involved makes the report useful on its own.

Assert, assume and cover

assert property says a rule must hold, and reports when it does not. assume property says the environment will behave in a certain way; formal tools use it to rule out impossible inputs, and simulators check it like an assertion.

cover property records that something happened, such as a stall of three cycles or an error response. Covers answer a different question. They ask whether the tests ever reached a situation, not whether a rule was broken.

Where assertions live

Designers put assertions inside RTL to state their own assumptions, such as "this FIFO pointer never passes that one". Verification engineers put protocol rules in the interface or in a separate checker module bound to the design.

Both kinds matter. Internal assertions catch a broken invariant at its source, while protocol assertions check every block that uses the interface, including blocks bought from someone else.

What assertions buy you

An assertion fails at the cycle where the rule broke, not thousands of cycles later at the scoreboard. That alone often turns a day of tracing back through a waveform into a few minutes.

Assertions can watch signals inside the DUT that never reach its outputs, through bind, which lesson A7.1 covers. The same properties also feed formal verification tools, which try to prove them for every possible input instead of only the ones a test happens to drive.

Try it

The concurrent assertions caught the dropped rvalid at the edge after the stall and the stray rlast at the edge where it appeared. The immediate assertion in the scoreboard caught the beat that arrived with nothing expected.

Each report names the rule and the time, so it points straight at the edge to inspect. Delete the line that drops rvalid and predict which reports remain.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic rvalid = 0, rlast = 0;
  last_ok: assert property (@(posedge clk) rlast |-> rvalid)
    else $display("fail at %0t", $time);
  initial begin
    @(negedge clk); rvalid = 1;
    @(negedge clk); rlast = 1;
    @(negedge clk); rvalid = 0;
    @(negedge clk); rlast = 0;
    #20 $finish;
  end
endmodule

!(rlast && !rvalid)

rvalid |-> rlast

rlast |-> rvalid

!rlast || rvalid