Why it matters

Three engineers each hold a failing trace. One starts at reset and ends in a broken FIFO; one starts in a state with the count at 14 that reset can never produce; one loops forever while a requester waits. The first demands an RTL fix, the second demands an invariant, the third demands a fairness argument. Treating all three as bugs fixes one, mis-fixes two, and misunderstands the engines behind them.

Job of this lesson: name the trace kind on sight and act correctly on each.

The core idea

A counterexample starts at reset and follows the design: unless the model is wrong, it is a real bug. A counterexample to induction (CTI) starts from arbitrary states, including unreachable ones, and its only duty is to show the step leaks; it may be spurious, and the cure is strengthening, not RTL surgery. A lasso is a finite prefix plus a loop, and it is how a liveness violation presents: the loop is the starvation, and the fairness constraints decide whether the loop is legal. The open flow in this course has no liveness engine and reports no lasso. A bounded-wait failure there is a finite safety counterexample: a requester waited longer than the bound, a trace with no loop. The lasso is the concept the engines section teaches; the course's runnable substitute is the bounded response.

Worked example: the three on small state spaces

The script models the real decade counter over all 16 states, including the enable that lets a state repeat. It finds the leak of the claim count != 15, rebuilds the chain from an unreachable start to the violation, and then tests invariants by the definition: an invariant is inductive when every step from every state satisfying it, for both enable values, stays inside it. The claim alone is not inductive, the range bound is, a bound that is too small is rejected, and the range bound implies the claim. The lasso half builds an arbiter state machine in which requester 3 is pending in every state of the loop and the grant alternates between two other requesters; the loop is starvation because no state of it grants requester 3. A fair rotation is tested as the counter-case, because its loop does grant requester 3:

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

def step(s, en):
    if not en:
        return s
    return 0 if s == 9 else (s + 1) % 16

STATES = range(16)

def inductive(inv):
    return all(inv(step(s, e)) for s in STATES if inv(s) for e in (0, 1))

never15 = lambda s: s != 15
reachable = {0}
frontier = [0]
while frontier:
    s = frontier.pop()
    for e in (0, 1):
        n = step(s, e)
        if n not in reachable:
            reachable.add(n)
            frontier.append(n)
assert sorted(reachable) == list(range(10))

leak = [s for s in STATES if never15(s) and not never15(step(s, 1))]
assert leak == [14] and 14 not in reachable                 # the CTI starts outside the reachable set
chain = [10]
while chain[-1] != 15:
    chain.append(step(chain[-1], 1))
assert chain == [10, 11, 12, 13, 14, 15]
assert not inductive(never15)                                # true but not inductive
assert inductive(lambda s: s <= 9)                           # the range invariant is
assert not inductive(lambda s: s <= 3) and not inductive(lambda s: s <= 13)
assert all(never15(s) for s in STATES if s <= 9)             # and it implies the claim

def lasso(next_state, start):
    seen, path, s = {}, [], start
    while s not in seen:
        seen[s] = len(path)
        path.append(s)
        s = next_state(s)
    return path[:seen[s]], path[seen[s]:]

def starves(loop, who):
    return all(req[who] and grant != who for req, grant in loop)

IDLE = ((0, 0, 0, 0), 0)

def unfair(s):                    # requester 3 keeps requesting; the grant alternates between 0 and 1
    req, grant = s
    if not any(req):
        return ((1, 1, 0, 1), 0)
    return (req, 1 if grant == 0 else 0)

def rotating(s):                  # fair: the grant rotates over all four requesters
    req, grant = s
    if not any(req):
        return ((1, 1, 1, 1), 0)
    return (req, (grant + 1) % 4)

prefix, loop = lasso(unfair, IDLE)
assert prefix == [IDLE] and len(loop) == 2 and starves(loop, 3)
prefix, loop = lasso(rotating, IDLE)
assert prefix == [IDLE] and len(loop) == 4 and not starves(loop, 3)
print("PASS: CTI chain 10 to 15 found and rejected; range invariant inductive; lasso starves requester 3")

What the review looks for

• Every failing trace is named as counterexample, induction counterexample, or lasso before it is acted on.

• Induction failures carry the starting state and whether any bounded run can reach it.

• Liveness claims name their fairness; unbounded eventuality without fairness is not filed.

Verify and debug

For an induction failure, enumerate the starting states by hand on the small model first: if they are unreachable, the design is innocent until a helper is proven. For a suspected lasso, mark the loop states explicitly and check each fairness constraint against them; a loop the fairness should have excluded is a harness gap, not a starvation.

Related topics

• Next: Four Counterexamples Worked

• Engines: K-Induction

• Engines: Liveness Engines