A team pointed the property checker at a deep arithmetic datapath and waited a week for an answer, while the control bug that later stopped the lab sat in a five-state handshake nobody had written a property for. The mistake was assignment, not effort. This lesson gives the split and a sizing rule.
Job of this lesson: say which obligations belong to formal and which stay in simulation, and size a formal model from its state bits before running anything.
Formal is strong where behaviour branches: control, protocols, arbiters, queues, connectivity, registers. The state is small enough to cover and the bugs hide in rare combinations. Simulation is strong where behaviour stretches: deep datapaths, long system flows, software-driven scenarios, where bugs need depth and data, not branching.
Obligation | Method | Why |
|---|---|---|
Control and protocol rules, handshake stability | Formal | Small state, exact sequences, rare stalls hide bugs. |
Arbiters, FIFOs, starvation and overflow | Formal | Exhaustive over inputs beats sampling rare combinations. |
Connectivity, register maps, reset values | Formal | Table-driven checks cover every mode at once. |
Wide datapath arithmetic | Equivalence checking or simulation | Wide multipliers blow up the solver; small ones are fine (a 4 by 4 multiplier pipeline is proved in this course in under 0.2 s). |
Long system flows, software-driven scenarios | Simulation | Depth beyond any bound; run the real sequence. |
Crossing protocol beside a synchroniser | Formal for the protocol | Prove the handshake; structural analysis covers the rest. |
State bits are the flip-flop bits of the design; the total is 2 to the number of bits; reachable states are those reachable from reset. The script derives both columns from the parts of each design and compares them with the counted values: the FIFO owns 39 bits but only 15.6 percent of its states are reachable, because the memory is never reset (20 control states times 2 to the 32 memory contents). It then injects a model that forgets the FIFO memory and shows the check catching it.
def products(width):
return len({a * b for a in range(2 ** width) for b in range(2 ** width)})
assert products(4) == 90
def reachable(start, step, inputs):
"""Breadth-first search of the control states reachable from reset."""
seen, todo = {start}, [start]
while todo:
state = todo.pop()
for inp in inputs:
nxt = step(state, inp)
if nxt not in seen:
seen.add(nxt)
todo.append(nxt)
return len(seen)
def fifo_step(state, inp, pop_works=True):
wptr, rptr, count = state
push, pop = inp
do_push = push and count < 4
do_pop = pop and count > 0 and pop_works
return ((wptr + do_push) % 4, (rptr + do_pop) % 4, count + do_push - do_pop)
def model(memory_bits=32, pop_works=True):
fifo = reachable((0, 0, 0), lambda s, i: fifo_step(s, i, pop_works), [(p, q) for p in (0, 1) for q in (0, 1)])
return { # name: (state bits, reachable states)
"sync_fifo": (memory_bits + 2 + 2 + 3, fifo * 2 ** memory_bits), # memory is never reset
"rr_arbiter": (2, reachable(3, lambda last, grant: grant, range(4))), # the pointer follows the last grant
"hs_bridge": (1 + 1 + 8 + 8, 3 * 2 ** 16), # 3 control states, data free
"csr_block": (8 + 2 + 8, 2 ** 18),
"pipe3": (4 + 4 + 8 + 8, 256 * products(4) ** 2 + 1),
"mod10_counter": (4, reachable(0, lambda c, run: (c + 1) % 10 if run else c, (0, 1))),
}
EXPECTED = { # the counted values the course quotes
"sync_fifo": (39, 549755813888, 85899345920, 15.6),
"rr_arbiter": (2, 4, 4, 100.0),
"hs_bridge": (18, 262144, 196608, 75.0),
"csr_block": (18, 262144, 262144, 100.0),
"pipe3": (24, 16777216, 2073601, 12.4),
"mod10_counter": (4, 16, 10, 62.5),
}
def check(designs):
for name, (bits, total, reach, share) in EXPECTED.items():
got_bits, got_reach = designs[name]
assert got_bits == bits, name
assert 2 ** got_bits == total, name
assert got_reach == reach, name
assert round(100.0 * got_reach / 2 ** got_bits, 1) == share, name
assert reachable((0, 0, 0), lambda s, i: fifo_step(s, i), [(0, 0), (1, 0), (0, 1), (1, 1)]) == 20
check(model())
for broken in (model(memory_bits=0), model(pop_works=False)): # a model without the memory, a FIFO that never pops
try:
check(broken)
raise SystemExit("FAIL: a wrong model was accepted")
except AssertionError:
pass
print("PASS: six designs sized from their parts, FIFO, arbiter and counter states found by search; two wrong models caught")Two readings fall out. First, size is a cost, not a verdict: 2 to the 39 states could be visited in minutes if only the visit counted; explicit search is impractical because of the visited set and the input choices (the next topic does that arithmetic), so the tool reasons about sets of states symbolically. Second, the reachable share matters for the induction step, which starts from all states; a bounded check follows the logic the property depends on (its cone of influence, defined later in this section) and the depth.
Every obligation names its method and one sentence of justification.
Each formal target states its state bits and reachable share before the first run.
Wide arithmetic and long flows go to equivalence checking or simulation, with the formal boundary drawn beside them.
When a formal run stalls, diagnose before tuning: read the cone size and the depth reached, then reduce, split, or strengthen in that order. Tightening assumptions to force a proof is the last resort and needs a written justification, because it risks hiding the bug the run was meant to find. If the cone is inherently wide, the obligation probably belongs elsewhere.
The controller and its protocol rules go to formal; the full-range counter is saturated or parameterised first, or its long flows stay in simulation.
The induction step starts from every state, reachable or not, so unreachable states cost it effort and can produce spurious traces; a bounded check never visits them. The count of reachable states is also what an explicit search would store.