How do you state a rule once and have it checked on every cycle of every test?

Every check so far compares one value after one edge and lives inside one testbench. The rule behind those checks, such as idle means hold, is checked only where somebody remembered to write it down. An assertion moves the rule itself into the simulator: stated once, then evaluated on every rising edge of every run, where a violation names the rule that broke and the time it broke.

A rule about signals over time

An assertion is a rule about signals over time, written in SystemVerilog Assertions (SVA), the assertion language inside SystemVerilog. A testbench check asks whether this cycle's value matches; an assertion states a relationship across cycles, such as an idle edge now means an unchanged count at the next edge, and the simulator enforces it everywhere the assertion is attached.

Each property below reads left to right through six pieces of vocabulary. assert property states a rule to enforce. @(posedge clk) samples it at every rising edge. disable iff (!rst_n) pauses it while reset is low, so reset edges are judged only by the property that defines reset. |=> means the consequent holds at the next edge. $past(count) is the count at the previous edge, and $stable(count) means the count did not change since then.

One property per row of the spec

The file holds four properties, one per row of the spec table. The reset property says a low reset at an edge means 0 at the next edge, and it is the only one without disable iff, because it is the property that states what reset does. Disabling it during reset would switch off exactly the cycles it must judge.

The clear property says a clear with reset inactive at an edge means 0 at the next edge. The counting property says a valid event with no clear at an edge means the old count plus 1 at the next edge, wrapping by width. The hold property says an idle edge with reset inactive means the count is unchanged at the next edge.

All four are written from the spec table, never from the RTL branch structure. An assertion copied from the design code repeats the design's mistakes with the authority of a rule, which is worse than no assertion at all.

How the hold rule is evaluated

The figure below walks through the hold property across two edges. At cycle n the antecedent is true: reset is high, clear and event are low. The arrow means the consequent is then checked at cycle n+1: is the count unchanged? If it moved, the assertion fires and names itself. Read it as a diagram of the rule, not as a simulated waveform: no signals are plotted over time.

What the assertion actually sees at each edge

One detail trips almost everyone. An assertion does not look at a value after the edge changes it. It samples every signal just before the edge, the same moment a flip-flop samples its input. So at edge n the assertion sees the old count, 3, and at edge n+1 it sees the count that edge n produced, 4. The $past(count) in the counting property is the sample from the previous edge, which is 3. The figure shows exactly this for the counting property, with event_valid high and clear_count low.

Four properties that judge every cycle

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

// Assertions for mini_controller. Needs a simulator with concurrent-assertion support
// (Verilator --assert); Icarus cannot parse these.
module mini_controller_sva (
    input logic       clk, rst_n, event_valid, clear_count,
    input logic [3:0] count
);
    a_reset: assert property (@(posedge clk) !rst_n |=> count == 4'd0);
    a_clear: assert property (@(posedge clk) disable iff (!rst_n)
                              clear_count |=> count == 4'd0);
    a_count: assert property (@(posedge clk) disable iff (!rst_n)
                              (!clear_count && event_valid) |=> count == $past(count) + 4'd1);
    a_hold:  assert property (@(posedge clk) disable iff (!rst_n)
                              (!clear_count && !event_valid) |=> $stable(count));
endmodule

This listing is the assertion module: four properties, one per spec row, each sampled at the rising edge with reset handled explicitly.

// Wrapper top that attaches the assertion module to the testbench's signals.
// Runs only on Verilator with --assert. Icarus cannot parse concurrent assertions.
// Note: a comment that STARTS with the word verilator is read as a pragma, so keep it off the first word.
module tb_with_sva;
    tb_mini_controller tb ();
    mini_controller_sva chk (.clk(tb.clk), .rst_n(tb.rst_n), .event_valid(tb.event_valid),
                             .clear_count(tb.clear_count), .count(tb.count));
endmodule

This wrapper attaches the assertion module to the testbench's signals, so every existing directed and random cycle is now also judged by the four rules. It needs the testbench module beside it, so it cannot compile alone and is shown as text. It runs only on Verilator with assertion support, because Icarus Verilog cannot parse concurrent assertions.

# captured terminal output
$ verilator --binary --timing --assert -Wno-fatal --Mdir build_ok --top-module tb_with_sva rtl/mini_controller.sv rtl/mini_controller_sva.sv tb/tb_mini_controller.sv tb/tb_with_sva.sv > /dev/null 2>&1; ./build_ok/Vtb_with_sva | grep -E 'PASS|ssert'
PASS: mini_controller

This output was measured on macOS, Verilator 5.048. The PASS line arrives with no assertion message, which means all four properties held on every cycle of the run: 239 directed and random edges, each judged four times.

Watch the assertion name the broken rule

The run below swaps in the idle_clears mutant and keeps everything else identical. Copy the message exactly: file, line, property name, and simulation time.

# captured terminal output
$ verilator --binary --timing --assert -Wno-fatal --Mdir build_bad --top-module tb_with_sva idle_clears.sv rtl/mini_controller_sva.sv tb/tb_mini_controller.sv tb/tb_with_sva.sv > /dev/null 2>&1; ./build_bad/Vtb_with_sva | grep -E 'PASS|ssert' | head -n 2
[1065000] %Error: mini_controller_sva.sv:12: Assertion failed in tb_with_sva.chk.a_hold: 'assert' failed.

This output was measured on macOS, Verilator 5.048. Line 12 of the assertion file is the hold property, and 1065000 is the simulation time of the first idle edge that cleared the count. A final value comparison would only say the run diverged somewhere; the assertion says which rule broke and when, which points straight at the hold logic.

Repeat the experiment yourself, then put the design back:

1. Copy mutants/idle_clears.sv over rtl/mini_controller.sv, keeping a copy of the original elsewhere.

2. Run the Verilator command above and confirm that a_hold fires at simulation time 1065000.

3. Restore the original design file and rerun to confirm the run passes with no assertion message before you continue.

Three ways an assertion checks nothing

• An antecedent that can never be true. A property whose left side never holds passes without checking anything, on every cycle, forever. Read each new assertion backwards: name one input combination in the testbench that makes the antecedent true, or the property is decoration.

• A missing `disable iff`. Without the reset guard, the other three properties judge reset edges too: during reset with idle inputs the count moves to 0 while the hold property demands no change, and the run fails on the design's most correct behavior. Guard every property that assumes reset is inactive.

• An assertion written from the RTL. A property copied from the design's branch structure restates the bug as a rule and passes on broken code. Write each property from its row of the spec table, the same table the reference model comes from.

Rule: write each spec row as an assertion, and every test checks it for free.

Key takeaways

• An assertion states a rule over time once, and the simulator checks it on every cycle of every test.

• Give each spec row its own property, written from the spec table, with disable iff where reset must be inactive.

• A firing assertion names the rule and the time, which points at the bug faster than a final mismatch.

Related topics

• RTL course: SVA for RTL

• Lesson 5.3, Random Stimulus and Seeds