A reviewer asks the question that decides whether a proof means anything: which states can this design actually reach? A property that holds on every reachable state is safe even if some unreachable state would break it. A property that breaks only in an unreachable state still fails induction, as the k-induction topic shows. Everything starts from the same picture: states, steps, and the set of states reachable from reset.
A synchronous design is a transition system. A state is the value of every register: the decade counter has 4 state bits, so 16 states, of which 10 (0 to 9) are reachable from reset and 6 (10 to 15) are not. The transition relation says which next states each state can step to under some input: with enable high the counter advances, with enable low it holds.
The reachable set is the smallest set that contains the reset state and is closed under steps: start from reset, add every successor, repeat until nothing new appears. That repetition is a fixed point, and it always terminates because there are only finitely many states. Safety is then one sentence: no bad state is in the reachable set. A bad state here is count 15, and the property count never 15 is the claim that 15 stays outside the reachable set. Liveness, covered later, is a claim about infinite paths, not about membership: it needs loops, called lassos, under fairness, and it cannot be reduced to one bad state.
The script below computes both directions on the 16 counter states with enable free. Forward from reset reaches exactly 0 to 9. Backward from the bad state 15 collects the states that can reach it: 10 to 15, none of them reachable from reset, which is why the property holds and also why induction struggles with it later. The injected variant models reset wrongly, with the start state left free: now 15 is reachable from the start, and the same check catches it.
def succ(s, last=9):
outs = {s} # enable low holds the count
outs.add(0 if s == last else (s + 1) % 16) # enable high advances
return outs
def forward(init, last=9):
seen = set(init)
frontier = list(init)
while frontier:
s = frontier.pop()
for t in succ(s, last):
if t not in seen:
seen.add(t)
frontier.append(t)
return seen
def backward(bad, last=9):
can = set(bad)
changed = True
while changed:
changed = False
for s in range(16):
if s not in can and any(t in can for t in succ(s, last)):
can.add(s)
changed = True
return can
good = forward({0})
assert good == set(range(10)), sorted(good)
assert 15 not in good
back = backward({15})
assert 0 not in back, "bad state reachable from reset"
# injected variant: start state left free instead of reset to 0
free = forward(set(range(16)))
caught = False
try:
assert 15 not in free # this must fail: a free start reaches 15
except AssertionError:
caught = True
assert caught, "checker did not catch the free-start model"
print("PASS: reachable set is 0..9, 15 outside it; free-start model reaches 15")The lesson names the state bits and the reset state before any engine is mentioned.
Reachable is distinguished from existing: 10 of 16 counter states are reachable, and the property is argued on the 10.
Every later claim about induction or abstraction refers back to this reachable set, not to intuition.
Recheck the reachable count against the covers the tool reports: the deepest first-reach step for count 9 is step 10, and the wrap cover needs step 14, so a bounded run shorter than depth 11 never sees the terminal pulse. If a counterexample starts in a state the enumeration above cannot reach, the reset model is wrong, not the design: the harness must hold reset in the first step and release it after, which the design files do with the init flag.
Backward collects states that could reach 15, including unreachable ones like 14. Unreachable states leading to a bad state do not threaten safety; they threaten induction, because the induction step starts from arbitrary states. That is the next topic's problem.