If SWMR is proved, is the protocol correct?

No. A controller that never grants anything satisfies SWMR and the data-value invariant forever: no writer, no reader, no wrong value. Coherence needs two kinds of property. Safety says nothing bad ever happens: SWMR, no stale read, no lost writeback, no response to a request that was never made. Liveness says something good eventually happens: every accepted GetS or GetM is eventually granted, every PutM eventually gets Put-Ack.

The difference in counterexample shape is the useful test. If you can show a violation with a finite trace, it is safety. If any finite prefix can still be rescued by something happening later, it is liveness: a GetM that has waited 10,000 cycles has not yet violated 'eventually granted'.

Writing both in SVA

1
2
3
4
5
6
7
8
9
10
11
12
13

// snippet
// Safety: an invariant, checked on every cycle (from the SWMR checker).
a_swmr: assert property (@(posedge clk) disable iff (!rst_n)
  $onehot0(wr) && (wr == '0 || rd == wr));
// Liveness: an accepted GetM from C1 is eventually granted (strong operator).
a_c1_getm_live: assert property (@(posedge clk) disable iff (!rst_n)
  c1_getm_accepted |-> s_eventually c1_grant_m);
// Fairness assumption on the environment (Part 5, A4): C1 eventually sinks Data.
asm_c1_sinks: assume property (@(posedge clk) disable iff (!rst_n)
  c1_data_valid |-> s_eventually c1_data_ready);
// Bounded substitute: granted within 64 cycles (illustrative bound).
a_c1_getm_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  c1_getm_accepted |-> ##[1:64] c1_grant_m);

s_eventually is SystemVerilog's strong 'eventually' (IEEE 1800-2017): the property fails if the good event never comes, including at the end of a finite simulation. The weak form exists only bounded, eventually [m:n]: a trace that ends inside the window passes. The unbounded form must be s_eventually. The same holds for the weak ##[1:N] consequent below: a request still pending when the simulation ends passes, so pair it with the end-of-test drain check (no transaction outstanding at the end). The bounded window is a safety property in disguise: a trace that reaches cycle 64 without a grant is a finite counterexample.

Why liveness needs fairness

Liveness is always conditional. C1's GetM completes only if messages are eventually delivered, H's arbiter eventually serves enabled work, buffers return credits and C1 eventually accepts its Data: assumptions A1 to A4 in Stating Progress Assumptions. In formal, those become assume properties. Without them the tool finds a trivial lasso, for example 'the network never delivers Inv-Ack', and the counterexample is about the environment, not your design.

Worked case on the course model: H's request arbiter for X sees GetM from C0 and from C1, one outstanding each. With fixed priority, C0 can win, get its grant, and request again before C1 is served, forever. That is a lasso: liveness fails, while SWMR holds on every state. With round robin, the program below proves there is no such loop and that C1 is granted within 2 arbitration steps, so ##[1:2] holds and ##[1:1] does not. Fixed priority satisfies liveness only under an extra fairness assumption that C0 eventually stops requesting, an assumption the real workload may break.

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

from itertools import product
# H's request arbiter for X: C0 and C1 each have at most one GetM waiting.
def steps(state, policy):
    p, last = state                         # p: pending flags, last: last grant
    pend = [i for i in (0, 1) if p[i]]
    if not pend:
        g = None
    elif policy == "fixed":
        g = pend[0]                         # C0 always wins
    else:
        g = next(i for i in ((last + 1) % 2, last) if p[i])  # round robin
    left = tuple(p[i] and i != g for i in (0, 1))
    for new in product((False, True), repeat=2):          # any arrivals
        yield g, (tuple(left[i] or new[i] for i in (0, 1)), last if g is None else g)
def reachable(policy):
    seen, todo = set(), [((False, False), 1)]
    while todo:
        s = todo.pop()
        if s not in seen:
            seen.add(s)
            todo += [t for _, t in steps(s, policy)]
    return seen
def c1_waits(policy):
    """Edges on which C1's request stays pending and is not granted."""
    return {s: [t for g, t in steps(s, policy) if g != 1]
            for s in reachable(policy) if s[0][1]}
def has_lasso(policy):                      # a cycle of C1-waiting states
    graph, colour = c1_waits(policy), {}
    def dfs(s):
        colour[s] = "grey"
        for t in graph[s]:
            if colour.get(t) == "grey" or (t not in colour and dfs(t)):
                return True
        colour[s] = "black"
        return False
    return any(s not in colour and dfs(s) for s in graph)
def worst_wait(policy):                     # steps until C1 is granted
    graph, memo = c1_waits(policy), {}
    def longest(s):
        if s not in memo:
            memo[s] = 1 + max((longest(t) for t in graph[s]), default=0)
        return memo[s]
    return max(longest(s) for s in graph)
assert has_lasso("fixed")                   # liveness fails: C1 can starve
assert not has_lasso("round-robin")         # every C1 request is granted
bound = worst_wait("round-robin")
assert bound == 2                           # so ##[1:2] holds, ##[1:1] fails
print(f"PASS: fixed priority starves C1 (lasso), round robin grants C1 within {bound} steps")

Why bounded checks are the practical substitute

Unbounded liveness proofs need fairness constraints, are harder for tools, and a pass says nothing about how long 'eventually' is. A bounded response property ##[1:N] gives a number that matters to the product (a watchdog limit, a latency budget), can be checked in simulation, and is easier to prove. Its weaknesses: N must come from an argument such as the one above, not from guessing; too small gives false failures, too large hides slow starvation; and it holds only under bounded environment assumptions (bounded delivery and acceptance), which are stronger than A1 to A4. Teams commonly use both: a bounded check as the everyday regression and an unbounded proof on a small model.

Related topics

• Shared course model

• Part 5: Stating Progress Assumptions

• Verification course: Bounded Proofs