The receiver from the hub diagram is written below three ways, and every spelling resets to IDLE with ready asserted. The one-process form keeps the state register and the three output registers in a single clocked block: each branch assigns the next state and the outputs together. The two-process form splits the work: a combinational block computes the next state, a single clocked line moves it into the state register, and three continuous assignments decode the outputs. The three-process form keeps that split and adds a second clocked block that samples the decoded outputs, so its pins settle one cycle after the two-process pins.
Read the three listings as three answers to where each piece of the machine lives. In the one-process listing the state update and the output update share every branch. In the two-process listing the state register is one isolated line, which is exactly the shape the FSM recognition passes look for later in this topic. In the three-process listing the output block samples the same decode one cycle later. The script after the listings maps all three against the teaching library and records what each spelling costs.
module pkt_1p (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;
always @(posedge clk) begin
if (rst) begin state <= IDLE; ready <= 1'b1; accept <= 1'b0; err <= 1'b0; end
else begin
ready <= 1'b0; accept <= 1'b0; err <= 1'b0;
case (state)
IDLE: begin ready <= 1'b1; if (start) state <= HDR; end
HDR: if (byte_valid) state <= PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) state <= CRC;
CRC: begin if (crc_ok) state <= DONE; else begin state <= IDLE; err <= 1'b1; end end
DONE: begin accept <= 1'b1; state <= IDLE; end
default: state <= IDLE;
endcase
end
end
endmodule
module pkt_2p (input wire clk, input wire rst, input wire start, input wire byte_valid, input wire last_byte, input wire crc_ok,
output wire ready, output wire accept, output wire 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;
case (state)
IDLE: if (start) next = HDR;
HDR: if (byte_valid) next = PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) next = CRC;
CRC: if (crc_ok) next = DONE; else next = IDLE;
DONE: next = IDLE;
default: next = IDLE;
endcase
end
assign ready = (state == IDLE);
assign accept = (state == DONE);
assign err = (state == CRC) && !crc_ok;
endmodule
module pkt_3p (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;
case (state)
IDLE: if (start) next = HDR;
HDR: if (byte_valid) next = PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) next = CRC;
CRC: if (crc_ok) next = DONE; else next = IDLE;
DONE: next = IDLE;
default: next = IDLE;
endcase
end
always @(posedge clk) begin
if (rst) begin ready <= 1'b1; accept <= 1'b0; err <= 1'b0; end
else begin ready <= (state == IDLE); accept <= (state == DONE); err <= (state == CRC) && !crc_ok; end
end
endmoduleread_verilog <<EOV
module pkt_1p (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;
always @(posedge clk) begin
if (rst) begin state <= IDLE; ready <= 1'b1; accept <= 1'b0; err <= 1'b0; end
else begin
ready <= 1'b0; accept <= 1'b0; err <= 1'b0;
case (state)
IDLE: begin ready <= 1'b1; if (start) state <= HDR; end
HDR: if (byte_valid) state <= PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) state <= CRC;
CRC: begin if (crc_ok) state <= DONE; else begin state <= IDLE; err <= 1'b1; end end
DONE: begin accept <= 1'b1; state <= IDLE; end
default: state <= IDLE;
endcase
end
end
endmodule
module pkt_2p (input wire clk, input wire rst, input wire start, input wire byte_valid, input wire last_byte, input wire crc_ok,
output wire ready, output wire accept, output wire 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;
case (state)
IDLE: if (start) next = HDR;
HDR: if (byte_valid) next = PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) next = CRC;
CRC: if (crc_ok) next = DONE; else next = IDLE;
DONE: next = IDLE;
default: next = IDLE;
endcase
end
assign ready = (state == IDLE);
assign accept = (state == DONE);
assign err = (state == CRC) && !crc_ok;
endmodule
module pkt_3p (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;
case (state)
IDLE: if (start) next = HDR;
HDR: if (byte_valid) next = PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) next = CRC;
CRC: if (crc_ok) next = DONE; else next = IDLE;
DONE: next = IDLE;
default: next = IDLE;
endcase
end
always @(posedge clk) begin
if (rst) begin ready <= 1'b1; accept <= 1'b0; err <= 1'b0; end
else begin ready <= (state == IDLE); accept <= (state == DONE); err <= (state == CRC) && !crc_ok; end
end
endmodule
EOV
design -save rtl
design -load rtl
hierarchy -top pkt_1p
proc
opt_clean
techmap
opt_clean
dfflibmap -liberty course.lib
tee -o abc_1p.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_1p.txt stat -liberty course.lib
write_json net_1p.json
select -assert-count 6 t:DFF
design -load rtl
hierarchy -top pkt_2p
proc
opt_clean
techmap
opt_clean
dfflibmap -liberty course.lib
tee -o abc_2p.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_2p.txt stat -liberty course.lib
write_json net_2p.json
select -assert-count 3 t:DFF
design -load rtl
hierarchy -top pkt_3p
proc
opt_clean
techmap
opt_clean
dfflibmap -liberty course.lib
tee -o abc_3p.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_3p.txt stat -liberty course.lib
write_json net_3p.json
select -assert-count 6 t:DFF
log PASS: one two and three process receivers map with six three and six flopsThe one-process form needs 6 flops and the three-process form needs 6, both with chip area 96, while the two-process form needs only 3 flops with chip area 66. The one-process and three-process reports match field for field, which the equivalence check below explains.
Style | Flops | ABC gates | ABC area | ABC delay | Chip area |
|---|---|---|---|---|---|
One-process | 6 | 21 | 48 | 492.11 ps | 96 |
Two-process | 3 | 18 | 42 | 506.03 ps | 66 |
Three-process | 6 | 21 | 48 | 492.11 ps | 96 |
Read the table from the flop column outward. The two-process receiver keeps 3 flops because only the state register is storage; everything else is gates. Either clocked-output spelling doubles that to 6 because ready, accept and err each take a flop, and the chip area follows from 66 to 96. The logic columns barely move: 18 against 21 ABC gates, because the same next-state decode and the same output decode exist in every spelling and only their landing place changes.
The drawing below is the recorded two-process netlist. The state lives in one three-bit register; the cloud of gates between it and the pins is the next-state and output decode. All three output pins are gate-driven, which is the whole structural difference to the other two spellings.
Identical reports suggest identical behaviour, and the script below proves it without simulating: it builds both receivers side by side, ties matching ports together with formal equivalence cells, and runs induction over them. The induction step covers every reachable state against every input combination, which no testbench author could enumerate by hand.
read_verilog <<EOV
module pkt_1p (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;
always @(posedge clk) begin
if (rst) begin state <= IDLE; ready <= 1'b1; accept <= 1'b0; err <= 1'b0; end
else begin
ready <= 1'b0; accept <= 1'b0; err <= 1'b0;
case (state)
IDLE: begin ready <= 1'b1; if (start) state <= HDR; end
HDR: if (byte_valid) state <= PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) state <= CRC;
CRC: begin if (crc_ok) state <= DONE; else begin state <= IDLE; err <= 1'b1; end end
DONE: begin accept <= 1'b1; state <= IDLE; end
default: state <= IDLE;
endcase
end
end
endmodule
EOV
hierarchy -top pkt_1p
proc
opt_clean
design -stash gold
read_verilog <<EOV
module pkt_3p (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;
case (state)
IDLE: if (start) next = HDR;
HDR: if (byte_valid) next = PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) next = CRC;
CRC: if (crc_ok) next = DONE; else next = IDLE;
DONE: next = IDLE;
default: next = IDLE;
endcase
end
always @(posedge clk) begin
if (rst) begin ready <= 1'b1; accept <= 1'b0; err <= 1'b0; end
else begin ready <= (state == IDLE); accept <= (state == DONE); err <= (state == CRC) && !crc_ok; end
end
endmodule
EOV
hierarchy -top pkt_3p
proc
opt_clean
design -copy-from gold pkt_1p
equiv_make pkt_1p pkt_3p equiv
hierarchy -top equiv
equiv_induct
equiv_status -assert
log PASS: one-process and three-process receivers agree on every cycleThe recorded run proves all six comparison points at once: the three state bits plus ready, accept and err agree on every cycle from reset, for every input sequence. The two-process form is deliberately not part of the proof, and the flop counts say why: with 3 flops against 6 it answers combinationally in the same cycle, while the other two spellings deliver the same answers one cycle later. Same machine, different timing, and the extra 3 flops are the receipt.
The two-process combinational block above opens with next holding its value and closes with a default arc to IDLE. The script below deletes both lines and records what the tools build instead. Nothing else changes: same states, same guards, same outputs.
read_verilog <<EOV
module pkt_nolatch (input wire clk, input wire rst, input wire start, input wire byte_valid, input wire last_byte, input wire crc_ok,
output wire ready, output wire accept, output wire 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
case (state)
IDLE: if (start) next = HDR;
HDR: if (byte_valid) next = PAYLOAD;
PAYLOAD: if (byte_valid && last_byte) next = CRC;
CRC: if (crc_ok) next = DONE; else next = IDLE;
DONE: next = IDLE;
endcase
end
assign ready = (state == IDLE);
assign accept = (state == DONE);
assign err = (state == CRC) && !crc_ok;
endmodule
EOV
hierarchy -top pkt_nolatch
proc
opt_clean
stat
select -assert-min 1 t:$dlatch
log PASS: missing preamble and default infers a latchThe assertion pins a level-sensitive latch on the next-state signal. The uncovered situations are every path through the block that never assigns next: the false branch of each guard (IDLE without start, HDR without byte_valid, PAYLOAD without last_byte) and the three unused codes. With no preamble and no default, those paths hold the old value of next, and holding a value without a clock is exactly what a latch does. The fix is the two deleted lines: assign next first, then override it per branch, and keep the default.
The two-process listing carries both output kinds. Ready and accept depend on the state alone: ready is high exactly while the machine sits in IDLE, accept exactly while it sits in DONE. Those are Moore outputs; they only move when the state moves. Err also watches an input: high while the machine sits in CRC and crc_ok stays low. That is a Mealy output, answering inside the cycle without waiting for a state move.
The price of the Mealy answer is a combinational path from an input pin to an output pin, which the output-registering lesson measures. The one-process and three-process spellings remove that path by construction: their outputs only change at clock edges. Name the kind per output, rather than per machine, to keep the trade visible when styles are mixed.
The extra 3 flops hold ready, accept and err inside the clocked block. The proof skips the two-process form because its combinational outputs answer a cycle earlier, so it cannot agree cycle by cycle with the clocked-output pair even though all three implement the same diagram.
A latch on the next-state signal: every path that skips next — a failed guard or an unused code — keeps the old value, and holding a value without a clock is storage, not gates. The preamble next = state and the default arc to IDLE together cover every path, so no hold is ever inferred.
Flop counts, ABC figures, chip areas, and netlists come from one recorded Yosys 0.70+post run mapping all three spellings against course.lib (typical.constr, loose 1000 ps target). Equivalence is a recorded equiv_make plus equiv_induct run proving six cells; the latch is a recorded preamble-and-default-deleted variant. Teaching library: absolute areas are units, orderings are the point.