Remembering data with local variables

Why a property needs memory

A response must match its request: the same ID, data from the requested address. Those values exist only at the request, and the check happens later.

With a fixed latency, $past(arid, 2) reaches back to the request. A local variable does the job more directly. It holds a value captured at one edge of an attempt for use later in the same attempt, and it can carry several values together.

Capturing with a match item

Declare local variables inside the property or sequence, before its clocking event: logic [3:0] id;. Assign them by listing the assignment after a condition in parentheses, (arvalid, a = araddr, id = arid). This match item runs at the edge where the condition matches, with that edge's sampled values.

Later parts of the attempt read the copy: (arvalid, id = arid) |-> ##2 (rvalid && rid == id). Every attempt that starts has its own id, so overlapping requests never mix, as the lanes above show.

Capture at the accepting edge

A request that waits for arready is offered at several edges but accepted at one. A rule that captures at every offer starts an attempt for each stalled edge, and each one expects a response that will never come.

(arvalid, id = arid)
  |-> ##2 (rvalid && rid == id)

(arvalid && arready, id = arid)
  |-> ##2 (rvalid && rid == id)

Measured on a request stalled for one edge: the left rule fails once, the right one never. The quiz below runs the same pair.

Where a local variable lives

Reading a design signal where a local variable was meant is the classic slip. rid == arid at the response compares with whatever request is on the bus now, which only works when nothing overlaps.

Local variable, $past or auxiliary code?

Three tools carry a value forward, and each has its place. $past(x, n) reads a fixed distance back. It needs no declaration, but it reads that edge whether or not a request was accepted there, so the rule has to repeat the acceptance condition through $past as well.

A local variable captures on a condition, carries several values together and gives every attempt its own copy. Auxiliary code, such as a counter or a small model, holds values that must outlive one attempt or be shared between assertions.

Start with the simplest tool that states the rule, and move up only when the rule needs it. A fixed-latency ID check is one $past. A check that also needs the address and the data is a local variable. Responses paired by their order need counters, as lesson A4.2 shows.

Delays that vary

A fixed latency, even one set per configuration with a parameter (##LAT), works with a local variable directly. When the latency varies from request to request, the response edge is unknown. For responses that return in request order, lesson A4.2 checks each request at its deadline instead, which needs only fixed delays.

Choosing what to capture

Capture only what the check needs, at the edge where the request is accepted. Name each variable after its meaning, such as a for the address and id for the ID.

Make the fail message carry the response side, for example "response for ID 4 carried data 95". With the request edge read off the waveform, that explains the bug on its own.

Try it

The first three requests were answered correctly, each checked by its own attempt even though they overlapped. The last three, made while bug was set, got data for the previous address, and each failure names the response's ID.

The fail action prints $sampled(rid), not id: the local variable is not visible there. Replace a in the consequent with $past(araddr, 2) and predict whether the output changes.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic       arvalid = 0, rvalid = 0;
  logic [3:0] arid = 0, rid = 0;
  property id_back;
    logic [3:0] id;
    @(posedge clk) (arvalid, id = arid) |-> ##2 (rvalid && rid == id);
  endproperty
  p: assert property (id_back) else $display("fail at %0t", $time);
  initial begin
    @(negedge clk); arvalid = 1; arid = 4;     // requests at 15 (ID 4) and 25 (ID 7)
    @(negedge clk); arid = 7;
    @(negedge clk); arvalid = 0; rvalid = 1; rid = 4;
    @(negedge clk); rid = 4;                   // the second response repeats ID 4
    @(negedge clk); rvalid = 0;
    #20 $finish;
  end
endmodule

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic       arvalid = 0, arready = 0;
  logic [3:0] arid = 0;
  // DUT: the response comes two edges after the accepting edge.
  logic       v1 = 0, v2 = 0;
  logic [3:0] i1 = 0, i2 = 0;
  always @(posedge clk) begin v1 <= arvalid && arready; i1 <= arid; v2 <= v1; i2 <= i1; end
  wire       rvalid = v2;
  wire [3:0] rid    = i2;
  int at_offer_fails, at_accept_fails;
  property at_offer;
    logic [3:0] id;
    @(posedge clk) (arvalid, id = arid) |-> ##2 (rvalid && rid == id);
  endproperty
  property at_accept;
    logic [3:0] id;
    @(posedge clk) (arvalid && arready, id = arid) |-> ##2 (rvalid && rid == id);
  endproperty
  offer:  assert property (at_offer)  else at_offer_fails++;
  accept: assert property (at_accept) else at_accept_fails++;
  initial begin
    @(negedge clk); arvalid = 1; arid = 6;   // offered at 15, not ready
    @(negedge clk); arready = 1;             // accepted at 25
    @(negedge clk); arvalid = 0; arready = 0;
    repeat (3) @(negedge clk);
    $display("offer=%0d accept=%0d", at_offer_fails, at_accept_fails);
    $finish;
  end
endmodule

a: assert property (@(posedge clk) arvalid |-> ##2 (rvalid && rid == arid)) else fails++;

a: assert property (@(posedge clk) $past(arvalid, 2) |-> (rvalid && rid == $past(arid, 2))) else fails++;

a: assert property (@(posedge clk) arvalid |-> ##2 (rvalid && rid == $past(arid, 2))) else fails++;

property id_back;
    logic [3:0] id;
    @(posedge clk) (arvalid, id = arid) |-> ##2 (rvalid && rid == id);
  endproperty
  a: assert property (id_back) else fails++;

Practice

• The right data for the right request Verify · Medium