SWMR in SWMR Precisely is a statement about all caches at one logical instant. To check it mechanically you need a single place that sees every cache's state for X at the same time, and a rule that turns each state into the permission it grants. That observer is a checker module bound into the system (or a function called by a model checker). It never drives the design; it only watches.
The property is written over permissions, not state names, so transient states must be mapped first. A load may hit in S, SM^D (loads hit, stores stall), E (MESI, MOESI), O and M; it may not hit in I, IS^D or IM^D. The eviction transients (PutM, PutE or PutS sent, waiting for Put-Ack, local accesses stalled) map as follows: MI^A is dirty but not readable, and the data in its writeback buffer must equal the ghost; EI^A is not readable; SI^A and II^A map to I. Writable means E or M. Dirty-responsible means M, O or MI^A. Forgetting that SM^D is readable gives a weak checker: it passes a broken grant that hands C0 M while C1 still sits in SM^D, serving loads from its old copy while it waits for its own upgrade.
Rule | Over all caches i for line X | Applies to |
|---|---|---|
SWMR, part 1 | At most one cache has writable permission (E or M) | MSI, MESI, MOESI |
SWMR, part 2 | If some cache is writable, no other cache can serve a load | MSI, MESI, MOESI |
Single dirty holder | At most one cache is in M, O or MI^A | MOESI, and every protocol once MI^A is counted (SWMR does not see MI^A beside an M) |
Data-value | Every cache that can serve a load holds the last value written to X | All, with a ghost variable |
MOESI changes part 2 only in what counts as a reader: O / 1 beside S / 1 is legal because neither may write. It adds the third row: two O copies are both read-only, so SWMR alone would pass them, yet each would believe it owes memory the writeback.
No hardware register holds 'the value X should have'. Memory is not it (write-back memory is legitimately stale), and the caches are what you are checking. So the checker keeps a ghost variable: verification-only state, invisible to the design, updated with the value of every store that is performed on X (X = 0 at reset). The property is then simple: every readable copy equals the ghost. The ghost is legal because SWMR guarantees only one writer, so 'the last store' is well defined. Without SWMR the ghost itself would be ambiguous, which is why the two invariants are checked together.
The module below is complete and lints with Verilator. It checks stable MOESI encodings plus a wb_dirty bit per cache; the caller maps transient states as described above (SM^D to S, IS^D, IM^D, EI^A, SI^A and II^A to I, MI^A to I with wb_dirty set and value carrying the writeback data). It assumes a cache's copy and the ghost both update on the clock edge after the store is performed.
// Safety checker for one address X across N caches (MOESI).
// The caller maps each cache's state to the permission it grants:
// SM^D -> S (loads hit), IS^D and IM^D -> I (no usable copy),
// MI^A -> I with wb_dirty set (dirty, not readable, value = its WB data),
// EI^A -> I (not readable), SI^A and II^A -> I.
module swmr_checker #(parameter int N = 2, parameter int W = 8) (
input logic clk,
input logic rst_n,
input logic [2:0] state [N], // 0 I, 1 S, 2 E, 3 O, 4 M
input logic [N-1:0] wb_dirty, // cache i is in MI^A: dirty data in its WB buffer
input logic [W-1:0] value [N], // cache i's copy of X, or its WB data in MI^A
input logic store_valid, // a store to X performed this cycle
input logic [W-1:0] store_data
);
localparam logic [2:0] ST_I = 3'd0, ST_E = 3'd2, ST_O = 3'd3, ST_M = 3'd4;
logic [N-1:0] wr, rd, dirty;
always_comb begin
for (int i = 0; i < N; i++) begin
wr[i] = (state[i] == ST_E) || (state[i] == ST_M);
rd[i] = (state[i] != ST_I); // S, E, O, M may serve loads
dirty[i] = (state[i] == ST_O) || (state[i] == ST_M) || wb_dirty[i];
end
end
// Ghost variable: the last value written to X (X = 0 at reset).
logic [W-1:0] ghost;
always_ff @(posedge clk)
if (!rst_n) ghost <= '0;
else if (store_valid) ghost <= store_data;
// SWMR: at most one writer, and a writer excludes every other reader.
a_swmr: assert property (@(posedge clk) disable iff (!rst_n)
$onehot0(wr) && (wr == '0 || rd == wr));
// At most one dirty-responsible holder: M, O or a dirty writeback (MI^A).
a_one_dirty: assert property (@(posedge clk) disable iff (!rst_n)
$onehot0(dirty));
for (genvar i = 0; i < N; i++) begin : g_dv
// Data-value: every usable copy and every dirty writeback holds the last value.
a_value: assert property (@(posedge clk) disable iff (!rst_n)
(rd[i] || wb_dirty[i]) |-> value[i] == ghost);
// Mapping check: MI^A is never readable.
a_wb_map: assert property (@(posedge clk) disable iff (!rst_n)
wb_dirty[i] |-> state[i] == ST_I);
end
endmoduleConcurrent assertions (assert property) are sampled on the clock and can be proved by a formal tool. The same Boolean can also be written as an immediate assertion inside an always_comb block, which checks it whenever the inputs change; that is useful in simulation, but a formal tool normally works with the clocked form. Both check one cycle at a time: these are invariants, not sequences.
Take the deliberately broken upgrade from What a Violation Looks Like (MSI, both caches S / 0, H skips the Inv and grants M to C0). That lesson shows the trace; here we only read the checker's verdict at each of its steps, keeping its step numbers and roles.
Step of the broken trace | C0 | C1 | Ghost | a_swmr | a_value |
|---|---|---|---|---|---|
Initial | S / 0 | S / 0 | 0 | pass | pass |
1. GetM received | SM^D / 0 | S / 0 | 0 | pass (two readers) | pass |
2. BUG Data received | M / 0 | S / 0 | 0 | FAIL: writer plus reader | pass (all copies 0) |
L. C0 store X=1 | M / 1 | S / 0 | 1 | FAIL | FAIL: C1 holds 0 |
The SWMR assertion fires at step 2, when the bits still agree. The value assertion fires one step later, after the store. A checker with only the value check would report the store as the bug; the real bug is the grant. The Python version below runs the same three checks (SWMR, single dirty holder and data value, kept separate as in the SVA) over that trace and over the correct upgrade from Invalidate Versus Update, and shows which check fails first.
WRITABLE = {"M", "E"}
READABLE = {"S", "SM^D", "E", "O", "M"} # states in which a load hits
DIRTY = {"M", "O", "MI^A"} # MI^A: dirty WB data, not readable
def swmr(states, values, ghost):
w = [i for i, s in enumerate(states) if s in WRITABLE]
r = [i for i, s in enumerate(states) if s in READABLE]
return len(w) <= 1 and (not w or r == w)
def one_dirty(states, values, ghost): # single dirty holder: a separate assertion
return sum(s in DIRTY for s in states) <= 1
def data_value(states, values, ghost):
return all(v == ghost for s, v in zip(states, values) if s in READABLE or s == "MI^A")
CHECKS = {"swmr": swmr, "one_dirty": one_dirty, "value": data_value}
ALL = ["swmr", "one_dirty", "value"]
def first_failure(trace, checks):
ghost = 0 # X = 0 at reset
for label, states, values, store in trace:
if store is not None:
ghost = store # ghost: last value written
for name in checks:
if not CHECKS[name](states, values, ghost):
return label, name
return None
# (label, states, values, value stored at this step or None)
broken = [("Initial", ("S", "S"), (0, 0), None),
("1. GetM at H", ("SM^D", "S"), (0, 0), None),
("2. BUG Data", ("M", "S"), (0, 0), None),
("L. C0 store 1", ("M", "S"), (1, 0), 1)]
correct = [("Initial", ("S", "S"), (0, 0), None),
("1. GetM at H", ("SM^D", "S"), (0, 0), None),
("2. Inv at C1", ("SM^D", "I"), (0, None), None),
("3. Inv-Ack at H", ("SM^D", "I"), (0, None), None),
("4. Data at C0", ("M", "I"), (0, None), None),
("L. C0 store 1", ("M", "I"), (1, None), 1)]
moesi = [("O and S", ("O", "S"), (0, 0), None),
("Two O", ("O", "O"), (0, 0), None)]
assert first_failure(correct, ALL) is None
assert first_failure(broken, ALL) == ("2. BUG Data", "swmr")
assert first_failure(broken, ["value"]) == ("L. C0 store 1", "value") # one step later
assert first_failure(moesi, ["swmr"]) is None # SWMR alone passes two O copies
assert first_failure(moesi, ALL) == ("Two O", "one_dirty")
evict = [("L. C0 store 1", ("M", "I"), (1, None), 1),
("C0 PutM sent", ("MI^A", "I"), (1, None), None), # legal: WB buffer holds 1
("BUG C1 M", ("MI^A", "M"), (1, 1), None)] # two dirty holders
assert first_failure(evict, ["swmr", "value"]) is None # SWMR does not see MI^A beside an M
assert first_failure(evict, ALL) == ("BUG C1 M", "one_dirty")
stale = [evict[0], ("C0 PutM sent", ("MI^A", "I"), (0, None), None)] # WB lost the store
assert first_failure(stale, ALL) == ("C0 PutM sent", "value")
assert first_failure([("w", ("M", "I"), (2, None), 2), ("lost", ("S", "S"), (1, 1), None)],
ALL) == ("lost", "value")
print("PASS: SWMR flags the early grant at step 2, the value check only at the store, one_dirty the two O and MI^A cases")False failure: after a store, C0 = M / 1 and memory = 0. That is legal write-back, but the check flags C0. Missed bug: the last store wrote 2, H then lost C0's dirty data, memory = 1 and both caches S / 1. Every copy agrees with memory, so the check passes, but the value 2 was lost. The ghost holds 2 and catches it.