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.
Checker | Rules | How | Built from |
|---|---|---|---|
ID scoreboard | R1, R2, R3, R5 | Queue per {port, id}; compare at the head; flush on reset | |
Memory model | R3 | Bytes updated at write acceptance; expected read data snapshotted at read acceptance | |
Watchdog and drain | R1 (liveness), R5 | Issue time per read; error after 200 cycles; leak or stuck at the end | |
a_no_orphan | R1, R5 | Assertion on auxiliary counters: a response needs a read outstanding on its ID | This lesson |
a_fair (two) | R6 | If one port waited while the other was accepted, the other is not accepted next cycle | This lesson |
a_rsp_stable | R4 | A stalled response keeps valid and its payload |
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.
All three ports are sampled at the same rising edge, and the order of processing matters:
Reset first. If rst_n is low, flush the scoreboard (R5) and record reset coverage. Nothing else happens in reset.
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.
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.
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.
// 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.
Checkers are code and need tests. This bench has no design. It drives the pins the capstone monitor watches from a script, one case per failure mode, and requires each case to be flagged by exactly the checkers expected, and the legal case by none.
// ===================== Checkers (from Checking Out-of-Order Traffic) =====================
class id_scoreboard #(type T = logic [31:0]);
string name;
protected T exp_q[int][$];
int n_added, n_matched, n_errors;
function new(string name); this.name = name; endfunction
virtual function void add_expected(int id, T item);
exp_q[id].push_back(item);
n_added++;
endfunction
virtual function void check_actual(int id, T item);
T exp;
if (!exp_q.exists(id) || exp_q[id].size() == 0) begin
n_errors++;
$display("%s: UNEXPECTED response for ID %0d with nothing outstanding (got %h)", name, id, item);
return;
end
exp = exp_q[id].pop_front();
if (exp_q[id].size() == 0) exp_q.delete(id);
if (item !== exp) begin
n_errors++;
$display("%s: MISMATCH ID %0d expected %h got %h", name, id, exp, item);
end else n_matched++;
endfunction
function int outstanding();
int n = 0;
foreach (exp_q[id]) n += exp_q[id].size();
return n;
endfunction
function int outstanding_on(int id);
return exp_q.exists(id) ? exp_q[id].size() : 0;
endfunction
virtual function void flush(); // reset: outstanding work is dropped by spec
exp_q.delete();
endfunction
endclass
class drain_scoreboard #(type T = logic [31:0]) extends id_scoreboard #(T);
protected longint issued_at[int][$];
longint last_progress;
int max_lat, late;
int leaked[$], stuck[$];
function new(string name, int max_lat);
super.new(name);
this.max_lat = max_lat;
endfunction
function void add_at(longint now, int id, T item);
add_expected(id, item);
issued_at[id].push_back(now);
endfunction
function void check_at(longint now, int id, T item);
check_actual(id, item);
if (issued_at.exists(id)) begin
void'(issued_at[id].pop_front());
if (issued_at[id].size() == 0) issued_at.delete(id);
end
last_progress = now;
endfunction
// Returns how many items passed max_lat on this cycle (each counted once).
function int watchdog(longint now);
int n = 0;
foreach (issued_at[id])
if (now - issued_at[id][0] == max_lat) begin
n++;
$display("%s: ID %0d waited %0d cycles (issued at %0d)", name, id, max_lat, issued_at[id][0]);
end
return n;
endfunction
virtual function void flush();
super.flush();
issued_at.delete();
endfunction
function void classify(longint now);
foreach (issued_at[id])
foreach (issued_at[id][k])
if (last_progress - issued_at[id][k] > max_lat) leaked.push_back(id);
else stuck.push_back(id);
foreach (leaked[i]) $display("%s: LEAK ID %0d never answered", name, leaked[i]);
if (stuck.size() != 0) $display("%s: STUCK IDs %p, no response for %0d cycles", name, stuck, now - last_progress);
endfunction
endclass
class mem_model;
protected bit [7:0] bytes[bit [31:0]];
function void write(bit [31:0] addr, bit [31:0] data, bit [3:0] strb);
for (int b = 0; b < 4; b++) if (strb[b]) bytes[addr + b] = data[8*b +: 8];
endfunction
function bit [31:0] read(bit [31:0] addr);
bit [31:0] w;
for (int b = 0; b < 4; b++) w[8*b +: 8] = bytes.exists(addr + b) ? bytes[addr + b] : 8'h00;
return w;
endfunction
endclass
The bench passes. The log shows each case and what fired:
Case | Scoreboard | a_no_orphan | Leak |
|---|---|---|---|
Legal cross-ID reorder | - | - | - |
Within-ID swap (bug 6) | MISMATCH x2 | - | - |
Duplicate response (bug 5) | UNEXPECTED | fires | - |
ID swap (bug 1) | UNEXPECTED | fires | - |
Strobe lane dropped (bug 2) | MISMATCH 88bb8888 vs 88888888 | - | - |
Response after reset | UNEXPECTED | fires | - |
Lost response (bug 3) | - | - | LEAK ID 0 |
Mutant run. Removing sb.flush() from the reset branch fails the bench on the reset case: the stale response matches the dropped read, the scoreboard stays quiet, and only a_no_orphan fires. That is exactly the escape a missing flush causes in a real regression, where a design that wrongly answers a dropped read would pass.
None in this bench: during reset nothing is sampled, and the controller holds rsp.valid low in reset. If the spec allowed responses during reset, the monitor would need a rule for them; R5 says outstanding reads are dropped, so a response for one after reset is UNEXPECTED.
The assertion's expected data is the controller's own memory at acceptance, which already contains the wrong byte. The scoreboard's expected data comes from the byte-level model updated with the strobes the testbench sent.