Lesson 3.6 · SystemVerilog Assertions Essentials

Local variables, parameters and good style

Local variables: remembering a value

Sometimes a property must remember data from an earlier tick — for example, to check that the response carries the tag of the request. SVA local variables capture a value when a sequence item matches:

local variable

// The response to a request returns the same tag, 1 to 4 ticks later
property p_tag_returned;
  logic [3:0] t;                                  // local variable
  @(posedge clk) disable iff (rst)
    (req_valid, t = req_tag)  |->  ##[1:4] (rsp_valid && rsp_tag == t);
endproperty
a_tag_returned: assert property (p_tag_returned);

Each attempt of the property gets its own copy of t, so overlapping requests are handled naturally. Local variables are powerful but can be expensive in formal; Chapter 6 shows a cheaper alternative for end-to-end data checks (a symbolic "tracked" value).

Parameterised properties with generate

generate loop

// One assertion per requester, generated from the parameter N
for (genvar i = 0; i < N; i++) begin : g_per_req
  a_gnt_only_if_req: assert property (gnt[i] |-> req[i]);
  c_gnt:             cover  property (gnt[i]);
end

Where do properties live?

Location	Pros	Cons
Inside the RTL	Designer intent close to code; travels with the design	Clutters RTL; must be synthesis-safe (tools ignore assertions in synthesis)
Separate checker module + `bind`	Clean separation; can be added without editing RTL	One more file to maintain
Formal wrapper module (as in this course)	Simple, portable across all tools including open-source ones	Can only see ports unless you reference internals hierarchically

bind

// Attach a checker to every instance of rr_arbiter without touching the RTL
bind rr_arbiter rr_arbiter_checker #(.N(N)) u_chk (.*);

Style rules that pay off

One idea per property. Small properties give clear failures and prove faster.
Name everything with the a_ / m_ / c_ convention and a meaningful suffix.
Mirror the spec. If the spec says "within 4 cycles", write ##[1:4], not a clever equivalent.
Avoid unbounded ranges in antecedents (a ##[0:$] b |-> c): they create many parallel threads and slow proofs. Track the condition with a small piece of modelling code instead.
Use modelling code freely. A few lines of auxiliary RTL (counters, flags) often make a property simpler and faster.
Pair assertions with covers of their antecedents.