An induction step once failed from a state the designer swore the design could never be in. The designer was right about runs from reset and wrong about the proof: the engine starts its step from arbitrary states, including ones reset can never produce. Until the team could draw the reachable region, every helper invariant looked like superstition. This lesson draws that picture.
Job of this lesson: define the model every engine works on: state, free inputs, next-state function, initial states, and reachable states.
A transition system has four parts: states (the register values), inputs (free every cycle unless assumed), a next-state rule (the clocked logic), and initial states (what reset produces). Reachable states are whatever the rule can produce from the initial states over any input sequence; everything else is unreachable, and an engine that starts anywhere still considers it.
The first line names the states, inputs, transition relation and initial states; the second says the reachable set is the least set that contains the initial states and every state one step from a state in it. Safety is an invariant, true in every reachable state; a counterexample is a finite path from an initial state to a state where it breaks. Liveness needs infinite paths, which a later topic treats.
The first script walks the decade counter breadth first (a queue, oldest state first, so the recorded depth is the shortest path). Ten states are reachable, 0 to 9, six are not, and the farthest is 9 transitions from reset. The check is applied to the counter and then to a mutant (a copy of the design with one planted bug) that wraps at 10: the mutant reaches eleven states and the check catches it.
from collections import deque
def bfs(init, step, inputs):
depth = {init: 0}
queue = deque([init])
while queue:
s = queue.popleft()
for i in inputs:
n = step(s, i)
if n not in depth:
depth[n] = depth[s] + 1
queue.append(n)
return depth
def counter(wrap):
return lambda s, en: s if en == 0 else (0 if s == wrap else s + 1)
def check(step):
depth = bfs(0, step, (0, 1))
assert sorted(depth) == list(range(10))
assert max(depth.values()) == 9
assert 15 not in depth
check(counter(9))
caught = False
try:
check(counter(10))
except AssertionError:
caught = True
assert caught
print("PASS: the counter reaches states 0 to 9 (diameter 9); the wrap-at-10 mutant reaches 11 states and is caught")The second script does the FIFO control machine, occupancy and read pointer (the write pointer is their sum, so it adds no states; the script confirms that by also searching with it). Twenty control states are reachable, the farthest, count 4 with read pointer 3, is 7 transitions from the reset state, and the longest shortest path is 7. A mutant without the full check reaches more states and a count above 4.
from collections import deque
def bfs(init, step, inputs):
depth = {init: 0}
queue = deque([init])
while queue:
s = queue.popleft()
for i in inputs:
n = step(s, i)
if n not in depth:
depth[n] = depth[s] + 1
queue.append(n)
return depth
def fifo(check_full=True):
def step(s, i):
count, rptr = s
push, pop = i
do_push = push and (count < 4 or not check_full)
do_pop = pop and count > 0
return ((count + do_push - do_pop) % 8, (rptr + do_pop) % 4)
return step
def fifo_with_wptr(s, i):
count, wptr, rptr = s
push, pop = i
do_push = push and count < 4
do_pop = pop and count > 0
return (count + do_push - do_pop, (wptr + do_push) % 4, (rptr + do_pop) % 4)
inputs = [(push, pop) for push in (0, 1) for pop in (0, 1)]
def check(step):
depth = bfs((0, 0), step, inputs)
assert len(depth) == 20
assert max(depth.values()) == 7
assert max(c for c, _ in depth) == 4
assert depth[(4, 3)] == 7
check(fifo())
caught = False
try:
check(fifo(check_full=False))
except AssertionError:
caught = True
assert caught
three = bfs((0, 0, 0), fifo_with_wptr, inputs)
assert len(three) == 20 and max(three.values()) == 7
print("PASS: 20 control states, diameter 7; the same with the write pointer added; a FIFO without the full check is caught")Now the same facts as proofs. count <= 9 alone is inductive: from any state with count at most 9 the next state is at most 9, so a prove 1 of that single property shows that 10 to 15 are unreachable.
// formal: prove 1 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= 4'd9);
`endif
endmoduleThe partner asks whether count 10 can be reached. Keep the cover in a file of its own: during a cover search the assertions of the same file act as constraints (measured: with a_range in the file, even the buggy counter does not reach 10 within 12). On the good design the cover is not reached within 20, which alone is inconclusive; read with the proof above, it is explained. On the mutant it is reached.
// formal: cover 20 expect fail slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) c_ten: cover (count == 4'd10);
`endif
endmodule// formal: cover 12 expect reached slang top mod10_counter define BUG=1
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) c_ten: cover (count == 4'd10);
`endif
endmoduleThe cover on the mutant is reached at step 11 (depth 11 is not enough, depth 12 is): the mutant visibly changes the reachable set.
States, inputs, the next-state rule and initial states are named before any property; unreachable states are named, not hand-waved.
Safety is an invariant over reachable states, and a cover about a state is read with the proof about it.
When an induction step fails, read where its trace starts: a start state outside the enumerated reachable set is spurious by construction, and the repair is a strengthening invariant, not a design fix. Re-run the enumeration after any change that touches reset or the state encoding.
Nowhere: they are unreachable from reset, because 9 wraps to 0 and nothing leads into 10 to 15. They still matter, because the induction step can start in them.
Not from the cover alone, which is inconclusive. The proof that count is at most 9 (inductive at k = 1) is what makes it a statement about all depths.