Which checker owns which rule

Every rule from the spec has one owner. Two owners for one rule is fine; zero is a hole that coverage cannot see, because coverage proves the state was reached, not that anything looked at it.

The watchdog limit of 200 cycles is about three times the worst latency seen in passing runs (69 cycles, the worst over seeds 1 to 30 and 99). The sink never stalls more than six cycles in a row, which keeps legal latency bounded.

Order of work in the monitor

All three ports are sampled at the same rising edge, and the order of processing matters:

1. Reset first. If rst_n is low, flush the scoreboard (R5) and record reset coverage. Nothing else happens in reset.

2. Responses next. A response at this edge belongs to a read accepted at an earlier edge, so it must be checked before this edge's requests change the queues.

3. Requests last. Writes update the memory model; reads take a snapshot of it and join their ID's queue. Only one request is accepted per cycle, so a write and a read never race inside one edge.

The scoreboard key is {port, id}, not id. Two ports both using ID 1 are different ordering domains; keying on id alone would merge them and report false within-ID swaps whenever the two ports interleave.

ID tracking with local variables

An assertion can enforce R1 with tickets. Each accepted read takes the next ticket number of its ID; the response that serves that ticket must come within the latency limit and carry the read's data. Local variables hold the ID, ticket and data for each attempt, so many reads can be in flight at once. Local Variables for IDs covers the technique; here it is bound into the controller.

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

// not-run: Verilator 5.048 warns SIDEEFFECT on the local-variable assignments in the match item and does not hold the captured values (the consequent saw the signals' current values in a directed test); Icarus 13 does not parse properties with local variables
// Ticket-based ID order check, bound into the controller (white box).
module ooo_id_order_sva #(parameter int MAX_LAT = 200) (
  input logic        clk, rst_n,
  input logic        rd_acc,              // a read accepted this cycle
  input logic [2:0]  acc_pid,             // its {port, id}
  input logic [31:0] acc_data,            // the data it must return (memory at acceptance)
  input logic        rsp_hs,              // a response handshake this cycle
  input logic [2:0]  rsp_pid,
  input logic [31:0] rsp_data
);
  // Auxiliary code: reads accepted and answered so far, per {port, id}.
  logic [7:0] n_acc [8], n_rsp [8];
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) for (int i = 0; i < 8; i++) begin n_acc[i] <= '0; n_rsp[i] <= '0; end
    else begin
      if (rd_acc) n_acc[acc_pid] <= n_acc[acc_pid] + 8'd1;
      if (rsp_hs) n_rsp[rsp_pid] <= n_rsp[rsp_pid] + 8'd1;
    end

  // Each read takes a ticket on its ID. The response that serves that ticket
  // must come within MAX_LAT cycles and carry the data captured at acceptance.
  property p_id_order;
    logic [2:0]  id;
    logic [7:0]  ticket;
    logic [31:0] data;
    @(posedge clk) disable iff (!rst_n)
      (rd_acc, id = acc_pid, ticket = n_acc[acc_pid], data = acc_data)
      |-> first_match(##[1:MAX_LAT] (rsp_hs && rsp_pid == id && n_rsp[id] == ticket))
          ##0 (rsp_data == data);
  endproperty
  a_id_order: assert property (p_id_order)
    else $error("ID %0d: response out of order, wrong data or missing", $sampled(rsp_pid));
endmodule

bind ooo_memctl ooo_id_order_sva u_id_order (
  .clk, .rst_n,
  .rd_acc  (acc && !a_write),
  .acc_pid ({a_port, a_id}),
  .acc_data(mem[a_addr]),
  .rsp_hs  (rsp.valid && rsp.ready),
  .rsp_pid ({rsp.port, rsp.id}),
  .rsp_data(rsp.data)
);

We could not run it. Verilator 5.048 compiles the property but prints SIDEEFFECT warnings on the match-item assignments, and a directed test showed the captured value was not held: when the source signal changed after the attempt started, the consequent compared against the new value and the assertion failed on legal traffic. Icarus 13 does not parse it. In the exact form above, with first_match and the ##0 data compare, Verilator never reported a failure at all, even for wrong data or a missing response, so a run that "passes" with it proves nothing. On a simulator that supports local variables, this is the property to add.

The same rule is enforced in the bench by the ID scoreboard, which is per-ID FIFO order plus data compare, and by a_no_orphan, which uses auxiliary counters instead of local variables and runs on Verilator. Note the property's data comes from the controller's own memory (mem[a_addr]), so it checks ordering and ID integrity, not memory correctness. A strobe bug writes the wrong byte into that memory and the assertion stays quiet; the scoreboard, whose expected data comes from an independent model, does not.

Related topics

• Previous: Environment Self-Test

• Next: Testing the Checkers

• Local Variables in Sequences

• Bind Fundamentals