Three bits hold eight codes and the receiver assigns five of them, so three codes, 5, 6 and 7, name no state. Those are the unreachable states of this lesson: codes the reset state can never walk to along the defined arcs. Three sources produce them in real hardware. The encoding itself leaves codes unassigned. Power-up puts unknown values on the flops before reset asserts. And a single-event upset can flip a state bit mid-flight, landing the machine on a code the designers never drew in the diagram.
Synthesis may also trim logic for codes it proves unreachable, which changes nothing functionally but removes any accidental safety net the gates might otherwise have provided. The program below makes the reachable set exact instead of hand-waved: it walks the transition function from the reset state over every combination of the four inputs, collects every code a walk can reach, and asserts the answer. Five states and sixteen input combinations are small enough to enumerate exactly, so no solver is needed and every claim below is checked, not hoped.
import sys
# Packet-receiver transition function over (state, start, byte_valid, last_byte, crc_ok).
STATES = ["IDLE", "HDR", "PAYLOAD", "CRC", "DONE"]
CODE = {"IDLE": 0, "HDR": 1, "PAYLOAD": 2, "CRC": 3, "DONE": 4}
def nxt(state, start, byte_valid, last_byte, crc_ok):
if state == "IDLE":
return "HDR" if start else "IDLE"
if state == "HDR":
return "PAYLOAD" if byte_valid else "HDR"
if state == "PAYLOAD":
return "CRC" if (byte_valid and last_byte) else "PAYLOAD"
if state == "CRC":
return "DONE" if crc_ok else "IDLE"
if state == "DONE":
return "IDLE"
return "IDLE" # default recovery arc
def reachable_from(start, hold_invalid):
seen = {start}
frontier = [start]
while frontier:
s = frontier.pop()
for a in range(16):
start_i, bv, lb, crc = (a >> 3) & 1, (a >> 2) & 1, (a >> 1) & 1, a & 1
if s in STATES:
t = nxt(s, start_i, bv, lb, crc)
else:
t = s if hold_invalid else "IDLE"
if t not in seen:
seen.add(t)
frontier.append(t)
return seen
from_reset = reachable_from("IDLE", False)
if from_reset != set(STATES):
print("FAIL: reachable " + str(sorted(from_reset)))
sys.exit(1)
codes_used = {CODE[s] for s in from_reset}
unreachable = sorted(set(range(8)) - codes_used)
if unreachable != [5, 6, 7]:
print("FAIL: unreachable " + str(unreachable))
sys.exit(1)
# An upset to code 5 with a default arc is home next cycle; holding sticks forever.
if not set(STATES) <= reachable_from(5, False):
print("FAIL: default recovery does not return")
sys.exit(1)
if reachable_from(5, True) != {5}:
print("FAIL: hold does not stick")
sys.exit(1)
print("PASS: reachable states are 0-4, unreachable are 5-7, default recovers and hold sticks")The asserted answer is that codes 0 to 4 are reachable and codes 5, 6 and 7 are not, and the program pins two more behaviours that the rest of the lesson prices. With the default arc in place, a machine knocked to code 5 walks home to the five known states on the very next cycle. With the hold behaviour of the no-default listing, the same upset sticks at code 5 forever: every input combination maps 5 back to 5, so no sequence recovers. Recovery is a property of the next-state logic, not of the reset line, and the three listings in the next script differ only in that logic.
The default and full-case runs match in every column with 18 ABC gates, while the hold run needs 21 gates and more chip area. The full-case run matches the default exactly in every column, which is precisely what makes it dangerous, as the last section explains.
read_verilog <<EOV
module pkt_u (input wire clk, input wire rst, input wire start, input wire byte_valid, input wire last_byte, input wire crc_ok,
output reg ready, output reg accept, output reg err);
localparam [2:0] IDLE = 3'd0, HDR = 3'd1, PAYLOAD = 3'd2, CRC = 3'd3, DONE = 3'd4;
reg [2:0] state, next;
always @(posedge clk) if (rst) state <= IDLE; else state <= next;
always @(*) begin
next = state; ready = 1'b0; accept = 1'b0; err = 1'b0;
case (state)
IDLE: begin ready = 1'b1; if (start) next = HDR; end
HDR: begin if (byte_valid) next = PAYLOAD; end
PAYLOAD: begin if (byte_valid && last_byte) next = CRC; end
CRC: begin if (crc_ok) next = DONE; else begin next = IDLE; err = !crc_ok; end end
DONE: begin accept = 1'b1; next = IDLE; end
default: next = IDLE;
endcase
end
endmodule
module pkt_hold (input wire clk, input wire rst, input wire start, input wire byte_valid, input wire last_byte, input wire crc_ok,
output reg ready, output reg accept, output reg err);
localparam [2:0] IDLE = 3'd0, HDR = 3'd1, PAYLOAD = 3'd2, CRC = 3'd3, DONE = 3'd4;
reg [2:0] state, next;
always @(posedge clk) if (rst) state <= IDLE; else state <= next;
always @(*) begin
next = state; ready = 1'b0; accept = 1'b0; err = 1'b0;
case (state)
IDLE: begin ready = 1'b1; if (start) next = HDR; end
HDR: begin if (byte_valid) next = PAYLOAD; end
PAYLOAD: begin if (byte_valid && last_byte) next = CRC; end
CRC: begin if (crc_ok) next = DONE; else begin next = IDLE; err = !crc_ok; end end
DONE: begin accept = 1'b1; next = IDLE; end
endcase
end
endmodule
module pkt_full (input wire clk, input wire rst, input wire start, input wire byte_valid, input wire last_byte, input wire crc_ok,
output reg ready, output reg accept, output reg err);
localparam [2:0] IDLE = 3'd0, HDR = 3'd1, PAYLOAD = 3'd2, CRC = 3'd3, DONE = 3'd4;
reg [2:0] state, next;
always @(posedge clk) if (rst) state <= IDLE; else state <= next;
always @(*) begin
next = state; ready = 1'b0; accept = 1'b0; err = 1'b0;
(* full_case *)
case (state)
IDLE: begin ready = 1'b1; if (start) next = HDR; end
HDR: begin if (byte_valid) next = PAYLOAD; end
PAYLOAD: begin if (byte_valid && last_byte) next = CRC; end
CRC: begin if (crc_ok) next = DONE; else begin next = IDLE; err = !crc_ok; end end
DONE: begin accept = 1'b1; next = IDLE; end
endcase
end
endmodule
EOV
design -save rtl
design -load rtl
hierarchy -top pkt_u
proc
opt_clean
techmap
opt_clean
dfflibmap -liberty course.lib
tee -o abc_def.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_def.txt stat -liberty course.lib
write_json net_def.json
select -assert-count 3 t:DFF
design -load rtl
hierarchy -top pkt_hold
proc
opt_clean
techmap
opt_clean
dfflibmap -liberty course.lib
tee -o abc_hold.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_hold.txt stat -liberty course.lib
write_json net_hold.json
select -assert-count 3 t:DFF
design -load rtl
hierarchy -top pkt_full
proc
opt_clean
techmap
opt_clean
dfflibmap -liberty course.lib
tee -o abc_full.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_full.txt stat -liberty course.lib
write_json net_full.json
select -assert-count 3 t:DFF
log PASS: default hold and full-case variants map with three flops eachRecovery | ABC gates | ABC area | ABC delay | Chip area |
|---|---|---|---|---|
Default to IDLE | 18 | 42 | 506.03 ps | 66 |
Hold on invalid | 21 | 54 | 505.58 ps | 78 |
full_case | 18 | 42 | 506.03 ps | 66 |
The default column is the baseline every later claim is measured against: 18 gates, area 42, delay 506.03 ps, chip area 66. The hold column shows what happens when invalid codes keep the current state instead of steering home: 21 gates and chip area 78, 12 units more, because every invalid code must feed the state back through a hold mux instead of landing on the constant zero. Recovery logic is never free; here it is exactly the gap between steering home and holding on. The hold run is a touch faster at 505.58 ps against 506.03 ps, which is a fair footnote but a bad trade: that sliver cannot buy back a machine that never recovers.
Cell | Default to IDLE | Hold on invalid |
|---|---|---|
AND2 | 1 | 0 |
AOI21 | 3 | 3 |
DFF | 3 | 3 |
INV | 5 | 4 |
NAND2 | 0 | 1 |
NAND3 | 2 | 2 |
NOR2 | 2 | 2 |
NOR3 | 5 | 6 |
OAI21 | 0 | 2 |
XNOR2 | 0 | 1 |
The histogram names the cells behind the gap. The hold cover adds two OAI21 cells, an XNOR2, a NAND2 and a NOR3 to build the feedback hold, while the default cover spends an AND2 and an extra inverter on the constant-steer instead. Both covers keep the same 3 state flops; the whole difference sits in the next-state cloud. That is the shape of the lesson in one sentence: the recovery choice is visible gate by gate, and the default to a constant state minimises better than the hold because a constant target simplifies while a feedback target must be built.
The recorded default netlist below closes the loop back to the diagram on the hub page: the state register, the next-state cloud with its recovery arcs, and the three output pins. Every invalid code has somewhere to go in this picture, which is exactly what the hold variant cannot say.
The full_case column matches the default column field for field, as the table shows: the attribute tells synthesis that codes 5 to 7 cannot occur, turning them into don't-cares the optimiser minimises freely, and on this machine the optimiser lands exactly where the explicit default lands. The covers agree, but the contracts do not. In simulation the full_case listing holds state on codes 5 to 7 through its preamble, so the simulation shows a machine stuck at code 5 while the gates — whose cover matches the default — most likely steer home on the next cycle: the two disagree, and that disagreement is the risk. Do not trust the area column alone: the attribute buys nothing here and risks a simulation-synthesis mismatch everywhere.
An in-flight bit flip to code 5, which reset cannot fix because reset asserted long ago. The hold variant maps 5 back to 5 on every input combination, as the program asserts, so the upset sticks forever while the default arc walks home next cycle.
Equal covers hide unequal contracts: full_case lets the optimiser assign don't-cares freely, so gates and simulation disagree on codes 5 to 7 while the explicit default steers them to IDLE in both. The area column cannot see the mismatch risk.
Reachability claims come from the asserted Python program shown. Cell counts, ABC figures, chip areas, histograms, and the netlist come from one recorded Yosys 0.70+post run mapping the default, hold, and full_case variants against course.lib with typical.constr. Absolute areas are teaching units.