Local Variables in Sequences

The problem local variables solve

Suppose a read request carries a tag and the response returns that tag 1 to 20 cycles later. You want: the response tag equals the request tag, and the response data equals what memory held . You cannot write this with $past because $past needs a constant cycle offset and the latency here is variable. You cannot use a module-level variable either, because several requests can be in flight at once and each needs its own remembered tag. Sequence local variables solve both problems: a variable declared inside a sequence or property is created fresh for every evaluation attempt, captured at a match item, and carried along that thread until the sequence ends.

// Variable-latency tag check — impossible with $past
property p_tag_match;
  logic [3:0] x;                       // local variable declaration
  @(posedge clk) disable iff (!rst_n)
    (req, x = req_tag)                 // capture at the cycle req is high
    |-> ##[1:20] (rsp && rsp_tag == x); // compare at the response
endproperty
ap_tag: assert property (p_tag_match)
  else $error("rsp_tag mismatch: expected %0h got %0h", $sampled(rsp_tag), $sampled(rsp_tag));

The syntax (expr, x = sig) is a sequence match item : when expr matches at a clock edge, the assignment executes using the sampled (preponed) value of sig at that same edge. Multiple assignments are allowed: (req, x = tag, y = addr).

Per-thread copies — each attempt gets its own x

A new evaluation attempt starts every clock edge, and within one attempt, ranges like ##[1:20] fork multiple threads. Every thread carries its own private copy of each local variable. Two overlapping requests therefore check independently — request A's thread remembers tag 5, request B's thread remembers tag 9, and neither interferes with the other.

PER-THREAD LOCAL VARIABLE COPIES

cycle      :  0    1    2    3    4    5    6
clk        :  ┐_┌─┐_┌─┐_┌─┐_┌─┐_┌─┐_┌─┐_┌─
req        :  1    1    0    0    0    0    0
req_tag    :  5    9    -    -    -    -    -
rsp        :  0    0    0    1    0    1    0
rsp_tag    :  -    -    -    9    -    5    -

Attempt @cycle 0:  thread A   x = 5
   waits ##[1:20] ... cycle 3: rsp, rsp_tag==9 → 9 != 5, thread continues*
                      cycle 5: rsp, rsp_tag==5 → MATCH, attempt PASSES

Attempt @cycle 1:  thread B   x = 9   (separate copy — NOT overwritten to 5)
                      cycle 3: rsp, rsp_tag==9 → MATCH, attempt PASSES

* with ##[1:20] the range forks a thread per delay value; the attempt
  passes if ANY thread matches. Each forked thread inherits its own
  copy of x as it existed at the fork point.

Contrast this with a module-level variable assigned in an always block: the second request would overwrite the stored tag before the first response arrived, and the check would corrupt itself. Per-thread copies are the entire point of the feature.

The canonical data-integrity pattern

The shape capture at request, compare at response is the single most reused SVA pattern in industry. It checks pipelines, caches, NoCs, out-of-order units — anything where data goes in, transforms predictably, and comes out later.

// Pipeline: output must equal input + 1, latency exactly 5
property p_pipe_data;
  logic [31:0] d;
  @(posedge clk) disable iff (!rst_n)
    (in_valid, d = in_data) |-> ##5 (out_valid && out_data == d + 1);
endproperty
ap_pipe: assert property (p_pipe_data);

// Bus: read data must match the last write to the same address
property p_rd_after_wr;
  logic [7:0]  a;
  logic [31:0] d;
  @(posedge clk) disable iff (!rst_n)
    (wr_en, a = wr_addr, d = wr_data)
    ##1 (!(wr_en && wr_addr == a)) [*0:$]   // no intervening write to a
    ##0 (rd_en && rd_addr == a)
    |-> ##1 (rd_data == d);
endproperty
ap_rdwr: assert property (p_rd_after_wr);

Walkthrough of p_rd_after_wr

1. Match item captures the write address and data the cycle wr_en is sampled high.

2. [*0:$] consumes any number of cycles during which no new write hits address a — a new write would make d stale.

3. ##0 fuses the read-enable check onto the last cycle of the repetition (goto-style end).

4. The consequent compares rd_data one cycle after the read — using the captured d, not a live signal.

Full example: FIFO data-integrity checker

A FIFO must deliver data in order. With local variables plus a small auxiliary counter, you can check that the N-th word out equals the N-th word in — without modeling the whole FIFO memory.

module fifo_data_check #(parameter DW = 32, DEPTH = 16) (
  input logic          clk, rst_n,
  input logic          push, pop,
  input logic [DW-1:0] din, dout
);
  // Auxiliary modeling: occupancy counter at time of each push.
  // The pushed word comes out after exactly 'count' pops.
  int unsigned count;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) count <= 0;
    else        count <= count + (push & ~pop) - (pop & ~push);

  property p_fifo_data;
    logic [DW-1:0] d;
    int unsigned   n;
    @(posedge clk) disable iff (!rst_n)
      (push, d = din, n = count)
      |-> first_match( ##[1:$] (pop && n == 0) ) ##0 (dout == d)
          or (pop && n == 0) [->1] ##0 (dout == d);
  endproperty
  // Simpler, the standard idiom: decrement n on every pop until it hits 0
  property p_fifo_data_v2;
    logic [DW-1:0] d;
    int unsigned   n;
    @(posedge clk) disable iff (!rst_n)
      (push, d = din, n = count)
      |-> ((!pop || n != 0), n = n - (pop ? 1 : 0)) [*0:$]
          ##1 (pop && n == 0 && dout == d);
  endproperty
  ap_fifo_data: assert property (p_fifo_data_v2)
    else $error("FIFO out-of-order or corrupt data");
endmodule

Note the second match item: n = n - (pop ? 1 : 0) — local variables can be reassigned at any match item, so n counts down the pops still ahead of our word. When n reaches 0, the next pop must produce our captured d. This counter-in-a-local-variable idiom is the standard answer to "check FIFO data integrity with SVA" and it works with any number of words in flight, because each pushed word's thread has its own n.

Restrictions and rules

• A local variable must be assigned before it is read — referencing an unassigned local is illegal.

• Assignment happens only in match items (seq, x = e) — you cannot assign locals from outside the sequence.

• A local variable is sampled like everything else: x = sig captures the preponed value of sig at that edge.

• Locals do not flow out of or/intersect branches unless assigned in ALL branches — the tool must know x has one defined value.

• Locals are invisible outside the property except via local variable formal arguments of subsequences; to print one on failure you typically re-derive or pass it to a subsequence.

• Each thread's copy dies when its thread dies — there is no global storage, hence no cleanup.

Interview angle

This is a top-three SVA interview topic. Expect: "Check that read data matches written data when the latency is variable" — the expected answer is a local variable, and saying $past is an instant red flag (it needs a constant offset). Expect "what happens if two requests overlap?" — answer: each evaluation attempt and each forked thread owns a private copy of the local, so overlapping transactions check independently. And expect the FIFO question: sketch the occupancy counter capture plus per-pop decrement idiom above. If you can write that cold, you have demonstrated real SVA fluency.

Key takeaways

• Local variables carry data through a sequence with variable latency — the job $past cannot do.

• Every evaluation attempt and every forked thread gets a private copy — overlapping transactions don't interfere.

• Assignment syntax is the match item: (expr, x = sig), sampling preponed values.

• The capture-at-request / compare-at-response shape is the canonical data-integrity pattern.

• Locals can be reassigned mid-sequence — counting down pops with n = n - 1 checks FIFO ordering.

Common pitfalls

• Using $past for variable-latency checks — it requires a constant cycle offset and silently checks the wrong cycle.

• Using a module variable instead of a local — the second in-flight transaction overwrites the first's captured data.

• Reading a local that was assigned in only one branch of an or — illegal, the variable has no defined value on the other branch.

• Forgetting that x = sig samples the preponed value — assigning inside the same edge the testbench drives sig gives last cycle's value.

• Unbounded ##[1:$] without a timeout in simulation — a lost response means the thread lives (and consumes memory) forever.