The variable-latency problem

A read request carries a tag and the response returns it 1 to 20 cycles later. The check must state that the response tag equals the request tag, whatever the delay.

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.

1
2
3
4
5
6
7
8
9

// snippet
property p_tag_match;
  logic [3:0] tag_mem;                 // local: one copy per attempt
  @(posedge clk) disable iff (!rst_n)
    (req, tag_mem = req_tag)           // capture the sampled tag
    |-> ##[1:20] (rsp && rsp_tag == tag_mem);
endproperty
ap_tag: assert property (p_tag_match)
  else $error("response tag did not match the requested tag");

The assignment runs when the left side matches, using the sampled value of the signal. A local is invisible in the action block, so the message above reports the fact, not the captured value.

One copy per thread

A new attempt starts every clock edge, and a range like ##[1:20] forks one thread per delay value. Every thread carries its own private copy of each local as it existed at the fork point.

If one forked thread sees the wrong tag, that thread simply fails. The attempt still passes through a sibling thread that matches.

The bottom two rows carry the answer. Tags keep the two attempts distinct.

• Slot 0: req is high with tag 5. The first attempt captures 5.

• Slot 1: req stays high with tag 9. The second attempt captures 9 in its own copy.

• Slot 2: both attempts wait while req is low.

• Slot 3: rsp returns tag 9. The second attempt matches and passes.

• Slot 4: the first attempt still waits while rsp is low.

• Slot 5: rsp returns tag 5. The first attempt matches and passes.

Capture at request, compare at response

Capture at request, compare at response is the single most reused SVA pattern. It checks pipelines, caches and queues: anything where data goes in, transforms predictably, and comes out later.

1
2
3
4
5
6
7

// snippet
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 + 32'b1);
endproperty
ap_pipe: assert property (p_pipe_data);

The FIFO listing below is not run in this course's checks: Verilator 5.048 does not support the unbounded [*0:$] repetition, and Icarus 13 has no SVA sequences.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

// not-run: Verilator 5.048 does not support unbounded [*0:$]; Icarus 13 has no SVA sequences
module fifo_data_check #(parameter int DW = 32) (
  input logic          clk, rst_n,
  input logic          push, pop,
  input logic [DW-1:0] din, dout,
  input logic [31:0]   count      // occupancy just before push, from nearby logic
);
  // At push, n holds the words ahead of ours. Each pop with n != 0 decrements
  // n in its own match item; the exit test reads n one cycle later, never in
  // the same item that writes it. The n != 0 guard matters: without it the pop
  // with n == 0 also continues the repetition, that thread never dies, and a
  // data mismatch on the exit thread could never fail the attempt.
  property p_fifo_data;
    logic [DW-1:0] d;
    logic [31:0]   n;
    @(posedge clk) disable iff (!rst_n)
      (push && !pop, d = din, n = count)
      |-> ((pop && n != 32'b0, n = n - 32'b1) or (!pop)) [*0:$]
          ##1 (pop && n == 32'b0) ##0 (dout == d);
  endproperty
  ap_fifo_data: assert property (p_fifo_data)
    else $error("FIFO data mismatch on pop");
endmodule

The illustration assumes push and pop never coincide on the push cycle. A word that never comes out leaves its thread open, so simulation runs add an outer timeout around this shape.

Common mistakes

Testbench

On Verilator 5.048, properties with local variables compiled but did not hold the captured value, so their verdicts were wrong. The bench below therefore does the local variable's job in modeling code: an array keeps the data each tag carried and a bit says its response is still owed, and a one-step assertion checks every response against them. On a simulator that runs local variables, the property form above is shorter; this form runs everywhere.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

// Two lanes with different latency; even tags take lane 0 (fast), odd tags lane 1 (slow).
module var_latency_pipe (
  input  logic       clk, rst_n, bug,
  input  logic       req,
  input  logic [3:0] req_tag,
  input  logic [7:0] req_data,
  output logic       rsp,
  output logic [3:0] rsp_tag,
  output logic [7:0] rsp_data,
  output logic       busy0, busy1
);
  logic lane0_valid, lane1_valid;
  logic [3:0] lane0_tag, lane1_tag;
  logic [7:0] lane0_data, lane1_data;
  logic [1:0] lane0_cnt, lane1_cnt;
  assign busy0 = lane0_valid;
  assign busy1 = lane1_valid;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin
      lane0_valid <= 0; lane1_valid <= 0; lane0_cnt <= 0; lane1_cnt <= 0;
      rsp <= 0; rsp_tag <= 0; rsp_data <= 0;
    end else begin
      rsp <= 0;
      if (lane0_valid && lane0_cnt == 0) begin
        rsp <= 1; rsp_tag <= lane0_tag; rsp_data <= lane0_data ^ (bug ? 8'h10 : 8'h00); lane0_valid <= 0;
      end else if (lane1_valid && lane1_cnt == 0) begin
        rsp <= 1; rsp_tag <= lane1_tag; rsp_data <= lane1_data; lane1_valid <= 0;
      end
      if (lane0_valid && lane0_cnt != 0) lane0_cnt <= lane0_cnt - 1;
      if (lane1_valid && lane1_cnt != 0) lane1_cnt <= lane1_cnt - 1;
      if (req && !req_tag[0] && !lane0_valid) begin
        lane0_valid <= 1; lane0_tag <= req_tag; lane0_data <= req_data; lane0_cnt <= 1;
      end
      if (req && req_tag[0] && !lane1_valid) begin
        lane1_valid <= 1; lane1_tag <= req_tag; lane1_data <= req_data; lane1_cnt <= 3;
      end
    end
endmodule

6 tagged requests over two lanes: 6 responses checked, 0 failures
one corrupted response: 1 failure
PASS: every response matched its own tag's data across variable latency, and the corrupted one was reported

Related topics

• Sampled value functions