Writing Properties and Sequences

The previous article wrote concurrent assertions inline, one per check. Real verification environments accumulate dozens of related temporal checks for one interface, and writing each as a standalone property gets unwieldy, and worse, hides which checks are variations of the same underlying pattern. Named sequence and property declarations are the fix, and they are the last piece of this module.

sequence: naming a temporal pattern

A sequence is a named, reusable version of the ##N expressions from the previous article:

sequence req_then_ack;
    req ##[1:4] ack;   // ack must follow req somewhere between 1 and 4 cycles later
endsequence

##[1:4] is new: a range rather than the fixed ##2. “Ack must occur somewhere in this window”, not “exactly this many cycles later”. That is often the more realistic requirement. A handshake response usually does not need to land on one exact cycle, only within an acceptable latency bound, and a range says that directly rather than forcing one arbitrary cycle count that happens to work for your test but is needlessly strict against the specification.

property: wrapping a sequence into a claim

A property takes a sequence, or a combination of them, and states the claim to check, usually with an implication:

property req_gets_ack;
    @(posedge clk) req |-> req_then_ack;
endproperty

assert property (req_gets_ack)
else $error("req was not followed by ack within the required 1-4 cycle window");

The sequence describes what pattern to look for; the property describes when the check applies and what to do on a violation. Separating the two means the same sequence can be reused in several properties with different surrounding conditions.

A small, coherent assertion library

This is where naming pays off. A few related sequences and properties for the Section 7.5 handshake, organised together rather than scattered as inline checks:

module handshake_assertions (
    input logic clk, rst_n,
    input logic req, ack
);
    sequence req_then_ack;
        req ##[1:4] ack;
    endsequence

    sequence ack_then_req_falls;
        ack ##1 !req;
    endsequence

    property p_req_gets_ack;
        @(posedge clk) disable iff (!rst_n)
        req |-> req_then_ack;
    endproperty

    property p_req_falls_after_ack;
        @(posedge clk) disable iff (!rst_n)
        ack |-> ack_then_req_falls;
    endproperty

    property p_req_held_until_ack;
        @(posedge clk) disable iff (!rst_n)
        $rose(req) |-> req until ack;     // req stays high on every cycle until ack arrives
    endproperty

    assert property (p_req_gets_ack)
    else $error("Handshake violation: req not acknowledged within 1-4 cycles");

    assert property (p_req_falls_after_ack)
    else $error("Handshake violation: req did not fall the cycle after ack");

    assert property (p_req_held_until_ack)
    else $error("Handshake violation: req dropped before ack arrived");

endmodule

Two things to note. disable iff (!rst_n) appears in every property. It tells the checker to ignore the property while reset is asserted, which is right, since signals are expected to be in an arbitrary, unsettled state during reset and checking protocol properties against that state would only produce spurious failures. This echoes the reset-awareness from the Section 8.4 reset-domain article, applied to assertions. And until in the third property (a SystemVerilog-2009 operator) reads as it sounds: req until ack means req must be true on every cycle up to the cycle ack becomes true.

This whole module can be instantiated once, bound to the handshake signals in a real design, and it will silently watch for any of the three violations across every test that ever exercises the handshake, the point from the first article in this section scaled up into an organised checker.

Assertions as executable documentation

The phrase worth keeping as this module closes: a well-organised assertion library like the one above is a specification written in a form the simulator can enforce. Not a comment that drifts out of sync with the real behaviour, and not a separate document nobody reads until something has gone wrong. A new engineer wanting to understand the handshake can read p_req_gets_ack, p_req_falls_after_ack and p_req_held_until_ack and know exactly what the protocol’s timing guarantees are, because those three properties are both the documentation and the mechanism checking every future change against it. IP blocks meant for reuse very often ship an assertion library alongside the RTL for exactly this reason, so any integrator can bind it and get a continuous check that they are using the block within its contract. Module 10’s UART, SPI and AXI4-Lite projects are a natural place to add your own.

Looking back over Module 9

Section 9.1 gave design-side SystemVerilog its cleanups: logic ending the wire/reg confusion, always_ff/always_comb/always_latch making intent explicit and checkable, struct/enum/union naming structured data instead of leaving it as loose bit vectors, and interface/modport bundling a protocol into one directionally safe declaration. Section 9.2 moved into new territory: classes for verification code, randomization and constraints generating volume and legality a directed test never could, assembled into the driver/monitor/scoreboard structure that is the ancestor of UVM. Section 9.3 closed with assertions: immediate checks living inside the design, and concurrent temporal properties checking multi-cycle behaviour, organised into named libraries that are specification and enforcement at once.

Before moving to Module 10, check yourself against this list:

1. What logic replaces, and the one case where wire is still required
2. What check always_comb adds that plain always @(*) cannot
3. Why unique case is the honest replacement for full_case/parallel_case
4. When to use struct versus union, and what typedef buys across a project
5. What a modport prevents that a plain interface bundle cannot
6. Why testbench code benefits from classes in a way RTL never does
7. The difference between rand and randc, and when each is right
8. What happens when randomize() is called against contradictory constraints
9. The driver/monitor/scoreboard split, and why checking does not belong in a driver
10. The difference between an immediate and a concurrent assertion
11. What |-> and |=> mean, and the one-cycle difference between them
12. Why disable iff (!rst_n) belongs in nearly every concurrent property
13. What “assertions as executable documentation” means in practice

Module 9 has given you the vocabulary to read essentially any modern SystemVerilog codebase: not UVM fluency, but working familiarity with every construct UVM is built from. In the next module we close the course with five complete projects, built from specification to verified simulation, using everything from the nine modules before it.