Pipelining inserts registers into combinational logic. Unlike retiming, it adds latency: each new register stage adds one cycle, and inputs that join late must be delayed to meet their stage. The cut points should balance the stages, because the slowest stage sets the period and an uneven split wastes the faster stages. The three-stage datapath below multiplies two pairs, adds the products, then adds a fifth input; a three-bit valid shift register walks alongside and marks which stages hold real results.
It beats it by the ratio of the two recordings: the unpipelined arrival against the slowest stage arrival, a small win here because the middle stage keeps both a multiply and an add. The proof below then checks something stronger than speed: every valid output equals the reference at the right latency.
read_verilog <<EOV
module s1(input [5:0] a, b, output [11:0] p);
assign p = a * b;
endmodule
module s2(input [11:0] p, input [5:0] c, d, output [11:0] s);
assign s = p + c * d;
endmodule
module s3(input [11:0] s, input [5:0] e, output [11:0] y);
assign y = s + e;
endmodule
module pipe3(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
reg [11:0] p, s, yq;
reg [2:0] v;
always @(posedge clk) begin
if (rst) begin p <= 0; s <= 0; yq <= 0; v <= 0; end
else begin
p <= a * b;
s <= p + c * d;
yq <= s + e;
v <= {v[1:0], v_in};
end
end
assign y = yq;
assign v_out = v[2];
endmodule
module ref3(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
reg [5:0] a2, b2, a3, b3, c1, d1;
reg [11:0] od;
reg [2:0] vv;
wire [11:0] yc;
assign yc = a3 * b3 + c1 * d1 + e;
always @(posedge clk) begin
if (rst) begin a2 <= 0; b2 <= 0; a3 <= 0; b3 <= 0; c1 <= 0; d1 <= 0; od <= 0; vv <= 0; end
else begin
a2 <= a; b2 <= b; a3 <= a2; b3 <= b2; c1 <= c; d1 <= d;
od <= yc;
vv <= {vv[1:0], v_in};
end
end
assign y = od;
assign v_out = vv[2];
endmodule
module pipe3w(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
wire [11:0] yi;
wire vi;
pipe3 p (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .d(d), .e(e), .v_in(v_in), .y(yi), .v_out(vi));
assign y = vi ? yi : 12'd0;
assign v_out = vi;
endmodule
module ref3w(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
wire [11:0] yi;
wire vi;
ref3 r (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .d(d), .e(e), .v_in(v_in), .y(yi), .v_out(vi));
assign y = vi ? yi : 12'd0;
assign v_out = vi;
endmodule
module pcomb(input [5:0] a, b, c, d, e, output [11:0] y);
assign y = a * b + c * d + e;
endmodule
EOV
hierarchy -check
proc
opt
techmap
opt
design -save all
hierarchy -check -top s1
tee -o ltp_s1.txt ltp
tee -o abc_s1.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_s1.txt stat -liberty course.lib
design -load all
hierarchy -check -top s2
tee -o ltp_s2.txt ltp
tee -o abc_s2.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_s2.txt stat -liberty course.lib
design -load all
hierarchy -check -top s3
tee -o ltp_s3.txt ltp
tee -o abc_s3.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_s3.txt stat -liberty course.lib
design -load all
hierarchy -check -top pipe3
tee -o stat_p3.txt stat
select -assert-count 39 t:$_SDFF_PP0_
design -load all
miter -equiv pipe3w ref3w miter
hierarchy -check -top miter
flatten
tee -o equiv_p3.txt sat -seq 6 -prove trigger 0 -prove-skip 1 -verify -set-init-zero -set in_rst 0 -set-at 1 in_rst 1
design -load all
hierarchy -check -top pcomb
tee -o ltp_comb.txt ltp
tee -o abc_comb.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_comb.txt stat -liberty course.lib
select -assert-none t:$mul t:$add
log PASS: three stages timed and pipeline proved over steps 2 to 6Each stage was timed on its own top, with the same library and load. The three ABC arrivals are 2084.11, 2637.22 and 1170.26 ps over 19, 24 and 10 topological levels; the unpipelined function needs 2835.42 ps over 26 levels. The pipelined period is the slowest stage, so the measured speedup is 1.08x: a small win, and the chart names the culprit. Stage 2 keeps both a multiply and an add, so the cut barely shortens the critical path. A better cut would isolate the second multiply into its own stage; the method below stays correct either way, and the placement decides what it earns.
Two independent metrics agree on the ranking, which is worth a pause. The topological level counts come from the generic netlists before any library mapping, while the picosecond arrivals come from ABC after mapping against the teaching library; neither knows about the other, yet both name stage 2 the slowest by a clear margin. When two such different lenses agree, the bottleneck is in the structure, not the measurement. That agreement is also what makes the modest speedup trustworthy: it is not a modelling artifact but the recorded consequence of leaving a multiply and an add in the same stage.
Stage | Logic | Topological levels | ABC delay (ps) | ABC area |
|---|---|---|---|---|
1 | a * b | 19 | 2084.11 | 532 |
2 | p + c * d | 24 | 2637.22 | 715 |
3 | s + e | 10 | 1170.26 | 137 |
Unpipelined | a * b + c * d + e | 26 | 2835.42 | 1358 |
The pipeline holds 39 flops across its data and valid registers, for 3 cycles of added latency. The reference model delays the early inputs to match: a and b wait two cycles, c and d wait one, e joins at once, and a three-deep valid shift marks the complete result. The wrappers mask both outputs with their valid bits, so fill cycles compare as 0 against 0; the check proves the valid-gated streams equal on steps 2 through 6 with reset asserted at step 1. With that short window only steps 5 and 6 carry valid results, so the proof checks two valid samples plus a masked fill, not a sustained rate. The rate evidence is the testbench below: 32 directed patterns plus a flush, with its own PASS line printed only when every valid output matches the skewed sum.
module pipe3(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
reg [11:0] p, s, yq;
reg [2:0] v;
always @(posedge clk) begin
if (rst) begin p <= 0; s <= 0; yq <= 0; v <= 0; end
else begin
p <= a * b;
s <= p + c * d;
yq <= s + e;
v <= {v[1:0], v_in};
end
end
assign y = yq;
assign v_out = v[2];
endmoduleThe second run below is the changed variant: both sides keep their valid-mask wrappers, and the only change is the reference latency, 2 instead of 3, with the same reset at step 1. The proof fails with a found model, and the recorded trigger stays high across steps 4, 5, 6: under changing inputs the valid outputs never line up: the masked fill still agrees, then the streams diverge once valid data emerges and stay diverged into steady state. Latency is not a comment in the header; it is the number the comparison is calibrated to, and 2 against 3 never passes.
read_verilog <<EOV
module pipe3(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
reg [11:0] p, s, yq;
reg [2:0] v;
always @(posedge clk) begin
if (rst) begin p <= 0; s <= 0; yq <= 0; v <= 0; end
else begin
p <= a * b;
s <= p + c * d;
yq <= s + e;
v <= {v[1:0], v_in};
end
end
assign y = yq;
assign v_out = v[2];
endmodule
module ref2(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
reg [11:0] p, s;
reg [1:0] vv;
always @(posedge clk) begin
if (rst) begin p <= 0; s <= 0; vv <= 0; end
else begin
p <= a * b;
s <= p + c * d;
vv <= {vv[0], v_in};
end
end
assign y = s + e;
assign v_out = vv[1];
endmodule
module ref2w(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
wire [11:0] yi;
wire vi;
ref2 r (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .d(d), .e(e), .v_in(v_in), .y(yi), .v_out(vi));
assign y = vi ? yi : 12'd0;
assign v_out = vi;
endmodule
module pipe3w2(input clk, input rst, input [5:0] a, b, c, d, e, input v_in, output [11:0] y, output v_out);
wire [11:0] yi;
wire vi;
pipe3 p (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .d(d), .e(e), .v_in(v_in), .y(yi), .v_out(vi));
assign y = vi ? yi : 12'd0;
assign v_out = vi;
endmodule
EOV
hierarchy -check
proc
opt
techmap
opt
miter -equiv pipe3w2 ref2w miter_b
hierarchy -check -top miter_b
flatten
tee -o equiv_lat2.txt sat -seq 6 -prove trigger 0 -prove-skip 1 -set-init-zero -set in_rst 0 -set-at 1 in_rst 1
log PASS: wrong-latency reference comparison recordedThe slowest stage sets it, so the period is 2637.22 ps against 2835.42 ps unpipelined: 1.08x. The gain is small because stage 2 keeps both a multiply and an add.
That the pipeline really adds 3 cycles: only the comparison calibrated to 3 agrees once valid data emerges, and any other number diverges there and stays diverged.
Stage levels, ABC delays and areas, flop counts, both sat outcomes, and the simulation PASS line on this page come from recorded runs of the blocks shown: one Yosys 0.70 run times all three stages plus the unpipelined function against course.lib with typical.constr and proves the valid-gated pipeline over steps 2 to 6, a second Yosys 0.70 run records the wrong-latency failure, and the testbench runs under the course simulators. The library is fictional, so absolute delays and areas are teaching units; the balance is the point.