A request/acknowledge interface between two blocks passes thousands of simulation runs. In the lab, once every few hours, a word goes missing. The waveform captured around the failure looks almost normal: a request rises and falls, the next request rises, and the receiver never captured the first one. No single test had produced that ordering of events, so no test had seen it.

How can you find the one ordering of events that breaks a protocol, without waiting for the lab to find it?

The obvious answer, and why it breaks

The obvious answer is more simulation: more seeds, longer runs, more random delays. Simulation explores the orderings your stimulus happens to create. Two independent sides, each with a few states and variable timing, produce many interleavings, and the dangerous ones are often rare, because they need one side to be unusually fast at exactly the moment the other is unusually slow. Random testing finds them eventually; the lab finds them sooner, at a much higher price.

The idea: a protocol is two state machines running together

Each side of an interface is a state machine: it is in one state, and the signals it sees move it to the next. The protocol is not either machine alone. It is the pair running side by side, called the product machine, whose state is (requester state, completer state, the signals between them). Every rule in the contract is an invariant on that product state: a condition that must hold in every state the pair can ever reach.

The product has a useful property: it is finite. For a small protocol you can list every reachable state by trying every move each side could make from every state, which is what a model checker does. If no reachable state breaks an invariant, the protocol is correct for every ordering of events, not only the ones a test produced.

The figure shows the two machines of a four-phase request/acknowledge protocol. The requester raises req with the data held stable, waits for ack, drops req, and waits for ack to fall before the next word. The completer captures the data when it sees req, raises ack, and drops ack when req falls.

The product, state by state

Ignoring the word counters, each side has a handful of control states, so the product has only six combinations. Walking through them shows which can actually occur and what each means:

The last row is the point of the exercise. The requester leaves WAIT LOW only after seeing ack low, so it can never be idle while the completer still holds ack high. That one unreachable state is what makes the protocol safe: a new request can never be mistaken for the old one.

Build it: explore every interleaving

The model below is a tiny model checker. From each state it tries every move either side could make, one at a time, in any order, and records every new state it reaches. It checks three promises: the completer captures only while the requester holds the data; no word is ever lost; and the pair never stops before all words are delivered. Then it repeats the search with a buggy requester that drops req without waiting for ack.

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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

"""Explore every interleaving of a requester and a completer joined by a
four-phase request/acknowledge handshake, and check three promises:
  1. the completer captures data only while the requester is holding it,
  2. no word is ever lost (every word sent is captured exactly once),
  3. the pair never deadlocks before all words are delivered.
Then repeat with a requester that drops req without waiting for ack.
"""
from collections import deque

N = 2  # words to send


def requester_moves(st, correct):
    r, c, req, ack, sent, cap = st
    if r == "IDLE" and sent < N:
        yield ("R raises req", ("REQ", c, 1, ack, sent + 1, cap))
    if r == "REQ" and (ack == 1 or not correct):
        yield ("R drops req", ("WAITLOW" if correct else "IDLE", c, 0, ack, sent, cap))
    if r == "WAITLOW" and ack == 0:
        yield ("R sees ack low", ("IDLE", c, req, ack, sent, cap))


def completer_moves(st):
    r, c, req, ack, sent, cap = st
    if c == "WAIT" and req == 1:
        yield ("C captures, raises ack", (r, "ACKED", req, 1, sent, cap + 1))
    if c == "ACKED" and req == 0:
        yield ("C drops ack", (r, "WAIT", req, 0, sent, cap))


def explore(correct):
    start = ("IDLE", "WAIT", 0, 0, 0, 0)
    parent = {start: None}
    queue = deque([start])
    violations = []
    while queue:
        st = queue.popleft()
        moves = list(requester_moves(st, correct)) + list(completer_moves(st))
        for label, nxt in moves:
            if label.startswith("C captures") and st[0] != "REQ":
                violations.append(("captured data the requester was not holding", st))
            if nxt not in parent:
                parent[nxt] = (st, label)
                queue.append(nxt)
        if not moves:  # nobody can move: the run has ended here
            r, c, req, ack, sent, cap = st
            if cap != sent:
                violations.append((f"lost word: sent {sent}, captured {cap}", st))
            elif sent != N:
                violations.append(("deadlock before all words were sent", st))
    return len(parent), violations, parent


def trace(parent, st):
    steps = []
    while parent[st] is not None:
        st, label = parent[st]
        steps.append(label)
    return list(reversed(steps))


n_ok, bad_ok, _ = explore(correct=True)
print(f"correct requester: {n_ok} reachable states, {len(bad_ok)} violations")
n_bug, bad_bug, parent = explore(correct=False)
print(f"buggy requester:   {n_bug} reachable states, {len(bad_bug)} violations")
what, st = bad_bug[0]
print(f"first violation: {what}")
print("  shortest path: " + " -> ".join(trace(parent, st)))
assert not bad_ok and bad_bug
print("PASS: the four-phase rules keep every promise; dropping req early loses a word")

It prints:

correct requester: 11 reachable states, 0 violations
buggy requester:   15 reachable states, 2 violations
first violation: lost word: sent 2, captured 0
  shortest path: R raises req -> R drops req -> R raises req -> R drops req
PASS: the four-phase rules keep every promise; dropping req early loses a word

The correct protocol has 11 reachable states (control states plus word counts) and no violations: every ordering of events, however unlikely, keeps every promise. The buggy requester reaches 15 states, two of which break a promise, and the search hands you the shortest path to the failure: the requester raises and drops req twice before the completer moves at all, so both words are sent and none is captured. That is the lab failure from the opening, found in milliseconds.

The design space: how to check a protocol

How real protocols use state machines

What breaks

The buggy requester in the model is not contrived (illustrative story). A designer optimised the requester to drop req one cycle after raising it, reasoning that the completer always responded within one cycle in the current system. The completer was later moved behind a synchroniser into a slower clock domain, where it sometimes needed several cycles to see req. Short requests then vanished entirely, exactly as in the model's counterexample.

The fix was to restore the rule "hold req until ack is seen". The deeper lesson: the optimisation was correct only for one timing of the other side. A protocol rule exists precisely so that each side stays correct for every timing of the other. Exploring the product machine makes that visible, because it does not assume any timing at all.

Key takeaways

• Each side of an interface is a state machine; the protocol is the product of the two, including the wires between them.

• Every rule of the contract is an invariant on the product; safety comes from dangerous states being unreachable.

• Exploring every interleaving finds races that random simulation reaches only by luck; a rule that holds only for one timing of the other side is a bug.

Related topics

• Part 0 overview: What Is a Protocol?

• CDC & RDC: Handshake Protocols Across Domains