A pipeline's contract is its latency: the output three cycles after an input is the specified function of that input, every time. The symptom of getting it wrong is a result attributed to the wrong input, found as occasional wrong answers under exactly the traffic the unit test skipped. History registers make the contract checkable: keep the last three inputs alongside the pipe and compare.
Count clean cycles since reset, because the output is only specified once the pipe has filled: before that the registers hold reset values, not results. Shift the low nibbles of every input through three history stages in plain registers, compute the expected result from the three-old values, and compare with the output. The reset property pins the output register at zero on the cycle after reset. The same history shape reappears in the equivalence section, where aligning two pipelines needs the same latency argument. This pipeline has no stall or flush input: a design that adds one must freeze its history with it, as the last question shows.
The pipeline property set proves with an induction depth of three: the base case covers the fill, and the induction step needs the full window because the output depends on three-old inputs. The history width is four bits per operand, matching the cone the function actually reads; the upper nibbles are optimisation-removed and excluded by construction:
// formal: prove 4 expect pass slang top pipe3
`define FORMAL
module pipe3 #(parameter CHECK = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
`ifdef FORMAL
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'd7);
end endgenerate
`endif
endmoduleTwo mistakes, each failing. First, a mutant that squares the stage sum instead of scaling it by the coefficient, the shape of a swapped stage operand: the timing is right and the value is wrong, and the latency property fails at step 4, the first step at which the output reflects an input. Second, the correct pipeline checked against a two-cycle claim: the history is one stage short, the window opens one step early, and the property fails at step 3 where the pipe has not yet delivered:
// formal: bmc 5 expect fail slang top pipe3_swap
`define FORMAL
module pipe3_swap (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * s[3:0];
y <= p + 8'd1;
end
end
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2, sa3, sb3, sc3;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
sa3 <= sa2; sb3 <= sb2; sc3 <= sc2;
end
wire [3:0] sum3 = sa3 + sb3;
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd3 && y == 8'h7);
endmodule// formal: bmc 4 expect fail slang top pipe3_lat2
`define FORMAL
module pipe3_lat2 (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output reg [7:0] y,
output wire [7:0] dbg_p
);
reg [7:0] s;
reg [3:0] c1;
reg [7:0] p;
assign dbg_p = p;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; p <= 8'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
p <= s[3:0] * c1;
y <= p + 8'd1;
end
end
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
reg [3:0] sa1, sb1, sc1, sa2, sb2, sc2;
always @(posedge clk) begin
sa1 <= a[3:0]; sb1 <= b[3:0]; sc1 <= c[3:0];
sa2 <= sa1; sb2 <= sb1; sc2 <= sc1;
end
wire [3:0] sum2 = sa2 + sb2;
always @(*) if (!init && hist == 2'd2) a_latency2: assert (y == (sum2 * sc2) + 8'd1);
always @(posedge clk) if (!init && $past(rst)) a_reset_zero: assert (y == 8'd0);
always @(*) if (!init) c_y_nonzero: cover (hist == 2'd2 && y == 8'h7);
endmoduleThe latency number is derived from the stage count, and the history depth matches it exactly.
The specified window excludes the fill: no assertion judges the output before the pipe is full.
The history covers exactly the bits the function reads: extra bits slow the proof for nothing.
A latency failure first asks which cycle the output reflects: count the registers between input and output in the trace, then check the history depth matches. A swapped-operand failure shows correct timing with wrong values: compare the expected expression term by term against the stage registers. A fill-window failure is the guard, not the logic: check the clean-cycle counter.
The history must freeze with the pipe: gate the shift registers and the clean-cycle counter with the stall, add a hold property for stalled outputs, and cover a stalled-then-drained sequence so the freeze is exercised, not assumed.