A read result depends on every earlier write to the same bytes, not on one matching request. The checker is a reference memory: writes update it, reads compare against it. Two questions decide whether it is right: how it stores bytes, and when it is updated.
Store bytes, not words, in an associative array keyed by byte address: bit [7:0] bytes[bit [31:0]]. Only written bytes use memory, so a 4 GB address space costs as much as the test touches. Byte granularity makes strobes and unaligned or mixed-width accesses straightforward.
A write with strobe wstrb[b] = 1 updates byte addr + b; a strobe of 0 leaves it alone.
A read of a never-written byte returns the reset or initial value the spec defines. Make it a parameter: some memories reset to zero, some are undefined, and for undefined bytes the honest check is to skip them.
bytes.num() is a cheap footprint check; see Memory Discipline for large tests.
The DUT below posts writes: it accepts a write into a two-entry buffer, and the array is updated later. A read must still see every write accepted before it, so the DUT forwards from the buffer, merging strobes oldest first. Read data returns two cycles after the read is accepted.
That gives two timing rules for the model:
Update on acceptance, not on completion. The protocol promises reads see accepted writes, so the moment of acceptance is the ordering point. A model updated when the buffer drains would expect stale data.
Snapshot the expected read value on acceptance and queue it. A write accepted between the read and its response must not change what that read expects.
cycle cmd model after cmd read 0x0 expects
10 READ 0x0 A A (snapshot now)
11 WRITE 0x0 = B B
12 (response) compare with A, not BCommands are 55% writes with random strobes to four hot words, which forces reads right behind buffered writes. After the random phase the bench reads every word back once the buffer has drained, so the array path is checked as well as the forwarding path. BAD_STRB plants a bug in the array update.
// 16-word memory with a 2-entry posted-write buffer.
// A write is accepted into the buffer and reaches the array later (one entry
// every other cycle). A read returns two cycles later and must see every
// accepted write: the array merged with matching buffer entries, oldest first.
// BAD_STRB >= 0 plants a bug: the array update ignores that strobe bit.
module posted_mem #(parameter int BAD_STRB = -1) (
input logic clk, rst_n,
input logic cmd_valid, cmd_write,
input logic [5:0] cmd_addr, // byte address, word aligned
input logic [31:0] cmd_wdata,
input logic [3:0] cmd_wstrb,
output logic cmd_ready,
output logic rsp_valid,
output logic [31:0] rsp_rdata
);
logic [31:0] mem [16];
logic bv [2];
logic [3:0] bidx[2];
logic [31:0] bdat[2];
logic [3:0] bstb[2];
logic phase;
logic [1:0] cnt;
logic r1_valid; // read pipeline stage
logic [31:0] r1_data;
assign cnt = 2'(bv[0]) + 2'(bv[1]);
assign cmd_ready = !(cmd_write && cnt == 2);
function automatic logic [31:0] merge(logic [31:0] w, logic [31:0] d, logic [3:0] s);
for (int b = 0; b < 4; b++) if (s[b]) w[8*b +: 8] = d[8*b +: 8];
return w;
endfunction
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
for (int i = 0; i < 16; i++) mem[i] <= 0;
bv[0] <= 0; bv[1] <= 0; phase <= 0; rsp_valid <= 0; rsp_rdata <= 0; r1_valid <= 0; r1_data <= 0;
end else begin
automatic logic drain = phase && bv[0];
automatic logic [3:0] idx = cmd_addr[5:2];
phase <= ~phase;
rsp_valid <= r1_valid;
rsp_rdata <= r1_data;
r1_valid <= 0;
if (cmd_valid && !cmd_write) begin
automatic logic [31:0] w = mem[idx];
for (int e = 0; e < 2; e++) if (bv[e] && bidx[e] == idx) w = merge(w, bdat[e], bstb[e]);
r1_valid <= 1;
r1_data <= w;
end
if (drain) begin
automatic logic [3:0] s = bstb[0];
if (BAD_STRB >= 0) s[BAD_STRB] = 1'b1; // planted bug
mem[bidx[0]] <= merge(mem[bidx[0]], bdat[0], s);
bv[0] <= bv[1]; bidx[0] <= bidx[1]; bdat[0] <= bdat[1]; bstb[0] <= bstb[1];
bv[1] <= 0;
end
if (cmd_valid && cmd_write && cmd_ready) begin
// tail slot after this cycle's drain
automatic int t = (drain ? int'(cnt) - 1 : int'(cnt));
bv[t] <= 1; bidx[t] <= idx; bdat[t] <= cmd_wdata; bstb[t] <= cmd_wstrb;
end
end
end
endmodule
// Sparse byte-level reference memory: only written bytes take storage.
class mem_model;
protected bit [7:0] bytes[bit [31:0]];
bit [7:0] init_value;
int n_reads, n_errors;
function new(bit [7:0] init_value = 8'h00);
this.init_value = init_value;
endfunction
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] : init_value;
return w;
endfunction
function void check(bit [31:0] addr, bit [31:0] expected, bit [31:0] actual);
n_reads++;
if (actual !== expected) begin
n_errors++;
$display("ERROR read %h: expected %h got %h (diff %h)", addr, expected, actual, expected ^ actual);
end
endfunction
function int bytes_used();
return bytes.num();
endfunction
endclass
The bench passes with 186 reads, 62 of them within three cycles of a write to the same word, and 218 partial-strobe writes. The model holds 16 bytes. Two mutants were run:
`BAD_STRB(2)`: the array update ignores strobe bit 2. The bench fails with 78 mismatches, and each diff sits in byte 2 only (for example diff 00ef0000). Reads served from the buffer were still correct; the bug appeared once data reached the array, which is why the drained read-back matters.
Snapshot at the response instead of acceptance: compute model.read(addr) when rsp_valid arrives. On the correct DUT this gives 23 false mismatches, all on reads followed by a write to the same word.
For that case, the model keeps a set of acceptable values per byte while a write is in flight. It narrows the set when the write completes:
// snippet: per-byte candidate values while a write to that byte is in flight
class relaxed_mem_model;
bit [7:0] settled[bit [31:0]]; // value after all completed writes
bit [7:0] pending[bit [31:0]][$]; // values of writes accepted but not completed
function bit read_ok(bit [31:0] a, bit [7:0] got);
if (settled.exists(a) && settled[a] == got) return 1;
if (!settled.exists(a) && got == 8'h00) return 1;
if (pending.exists(a)) foreach (pending[a][i]) if (pending[a][i] == got) return 1;
return 0;
endfunction
endclassThis is weaker than the exact check, so use it only where the spec really allows both answers, and add coverage that both outcomes occur.
Forwarding merges the buffered data with its correct strobes. The bad strobe only affects the array update, so only reads after the entry drains see the extra byte.
Strobes and narrow or unaligned accesses then need no read-modify-write logic in the model, and a model of a wider or narrower bus reuses the same store. Words would need masking that can repeat the DUT's own bugs.