The problem

A responder accepts up to four requests, each tagged with an ID, and answers them in any order after a variable delay. The rule is: the response carrying a request's ID must carry that request's data, transformed by the DUT. A fixed $past(data, N) cannot express this, because N changes per request and other requests interleave.

One copy per attempt

A local variable is declared inside a sequence or property. At the start of each evaluation attempt a new copy is created (16.10). Four requests in flight are four attempts, each holding its own id and data. That is what makes local variables the natural tool for out-of-order checking: the simulator keeps one thread per transaction for you.

Loose form and strict form

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

// not-run: Verilator 5.048 compiles local variables but did not hold the captured value in our test (the check used the source signal's current value), so verdicts are wrong; Icarus 13 has no concurrent assertions
// Loose: some response with this ID and the right data appears within 16 cycles.
property p_id_loose;
  logic [1:0] id;
  logic [7:0] d;
  @(posedge clk) disable iff (!rst_n)
    (req_valid, id = req_id, d = req_data) |->
      ##[1:16] (rsp_valid && rsp_id == id && rsp_data == d + 8'h11);
endproperty

// Strict: the FIRST response with this ID arrives within 16 cycles and is correct.
property p_id_first;
  logic [1:0] id;
  logic [7:0] d;
  @(posedge clk) disable iff (!rst_n)
    (req_valid, id = req_id, d = req_data) |=>
      (!(rsp_valid && rsp_id == id))[*0:15]
      ##1 (rsp_valid && rsp_id == id && rsp_data == d + 8'h11);
endproperty

a_id: assert property (p_id_first);

The loose form passes if a wrong response is followed by a correct one, because ##[1:16] succeeds on any match. The strict form allows no response with that ID until the one that must be correct; a wrong first response ends the repetition and fails the attempt. Both are bounded: a lost response fails after 16 cycles. With ##[1:$] instead, the property is weak in an assert (16.12.1), so a lost response never fails in simulation.

What local variables cannot say

Each attempt sees one transaction. Rules about the ID table as a whole need state shared across transactions, which local variables cannot hold:

• No reuse: a request must not use an ID that is still outstanding. In formal this is an assumption on the environment.

• No unsolicited response: a response must carry an outstanding ID.

• No duplicate: once answered, an ID is free; a second response with it is unsolicited.

These need auxiliary code: an outstanding bit per ID, set on request and cleared on response, plus simple one-cycle assertions. Production checkers combine both: local-variable properties for per-transaction data, aux code for table invariants. The strict property above also relies on no-reuse; with reuse, a second request's response could be taken as the first's.

Cost

Each request starts one attempt that lives until its response or the bound. Outstanding depth times window length is the thread count the simulator carries. Keep the window as tight as the spec allows, and never leave it unbounded: an unbounded weak attempt that never completes costs memory for the rest of the run and reports nothing.

Running it here

In our test with Verilator 5.048, a property captured req_data = 0x11, the input then moved to 0x55, and the response correctly returned 0x11. The assertion failed, which a correct tool would not do: the check had used the current value of the input instead of the captured copy. So the bench below does not run the local-variable property. It runs the same rule two other ways and requires both to agree:

• Aux code: an expected-data table and an age counter per ID, read by one-cycle assertions. This is the form many teams use in production and with formal tools.

• One thread per request: an automatic task forked for each request, holding its own id and d, waiting up to 16 cycles for the first response with that ID. This is the per-attempt semantics of p_id_first written out in procedural code.

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
39
40
41
42
43
44
45
46
47
48
49

// Out-of-order responder: up to 4 requests in flight, one per ID.
// Each ID waits a data-dependent latency; the lowest ready ID responds.
module ooo_resp (
  input  logic       clk,
  input  logic       rst_n,
  input  logic       req_valid,
  input  logic [1:0] req_id,
  input  logic [7:0] req_data,
  output logic       rsp_valid,
  output logic [1:0] rsp_id,
  output logic [7:0] rsp_data
);
  logic [3:0] busy;
  logic [7:0] store  [4];
  logic [2:0] wait_q [4];
  logic       pick_ok;
  logic [1:0] pick;
  always_comb begin
    pick_ok = 0;
    pick    = 0;
    for (int i = 3; i >= 0; i--)
      if (busy[i] && wait_q[i] == 0) begin
        pick_ok = 1;
        pick    = 2'(i);
      end
  end
  always_ff @(posedge clk) begin
    if (!rst_n) begin
      busy      <= '0;
      rsp_valid <= 0;
      rsp_id    <= 0;
      rsp_data  <= 0;
    end else begin
      for (int i = 0; i < 4; i++)
        if (busy[i] && wait_q[i] != 0) wait_q[i] <= wait_q[i] - 1;
      rsp_valid <= pick_ok;
      if (pick_ok) begin
        rsp_id     <= pick;
        rsp_data   <= store[pick] + 8'h11;
        busy[pick] <= 0;
      end
      if (req_valid) begin
        busy[req_id]   <= 1;
        store[req_id]  <= req_data;
        wait_q[req_id] <= req_data[2:0] ^ {req_id, 1'b1};
      end
    end
  end
endmodule

In the run, 171 requests are answered and 34 responses come back ahead of an older outstanding request. To make it fail, change the DUT so a response for ID 2 returns ID 3's stored data (store[pick == 2 ? 2'd3 : pick]): both checks report 38 failures.

Related topics

• Previous: let and Property Libraries

• Next: Formal-Ready Assertions

• Local Variables in Sequences (Part 4)

• ID-Tagged Scoreboard