A datapath rule says the output equals a function of the inputs three cycles ago. The textbook form writes that as a delay chain, and the proof engine rejects the operators outright. The engineer who concludes that latency cannot be proved formally has confused the notation with the check. This lesson's one job is the compilation: every delay becomes a flop, every range an OR over history bits, every repetition a counter, and the pipeline proof goes through on history registers alone.
A sequence is a pipeline of match bits. The expression a followed by b one cycle later followed by c is three one-bit registers in series: the first records that a fired, the second that a fired and then b fired, the third that the whole chain completed. The proof never sees the chain; it sees three flops and one comparator on the last. A consecutive repetition is the same idea folded into a counter: count the run length, compare against the bound.
A range delay is a disjunction over history. Waiting one to three cycles for an event is three history bits ORed together: the request one cycle back, two cycles back, or three cycles back, combined with the grant now. The width of the OR is the width of the window, and nothing else changes.
Two numbers are easy to confuse. The history depth belongs to the rule: how many past samples the check reads, here three. The proof window k belongs to the induction: how many consecutive steps the engine unrolls. The history registers are ordinary state that the step may start from an arbitrary value, so the step ties the output to real earlier inputs only when the window reaches back through the whole pipeline: three here, as the runs below measure.
The arithmetic pipeline takes three cycles from inputs to output: a word presented in cycle t appears transformed in cycle t plus 3. The textbook delay chain reads naturally and does not run on this front end:
// not-run: delay operators are not accepted by this front end
// textbook: req ##1 stage1 ##1 stage2 ##1 y_matches
// checks cycles t, t+1, t+2 and t+3 against the input of cycle tThe runnable form keeps the same meaning with plain history registers: three stages of input flops record what a, b and c were three cycles ago, a history-valid counter skips the fill cycles after reset, and one combinational check compares the output against the function of the recorded inputs. On the correct pipeline the proof passes:
// formal: prove 4 expect pass slang top pipe3
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
// Lesson-local parameter: BUG=1 makes the multiplier ignore bit 3 of the stage-1 copy of c.
module pipe3 #(parameter CHECK = 1, parameter BUG = 0) (
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 // stage-2 register, exposed for the miter's helper invariant
);
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] * ((BUG == 1) ? {1'b0, c1[2:0]} : c1);
y <= p + 8'd1;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history, as plain registers (works in every front 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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// after reset the output register is 0
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
endmodule
module pipe3_retimed #(parameter BUG = 0) (
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 [3:0] dbg_s2, // stage-2 registers, exposed for the miter's helper invariant
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
// helper invariant across the moved cut: the reference's stage-2 register p equals the
// twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmoduleThe induction needs a window of three. Re-run with a window of two and the base case still passes while the step fails: the step starts mid-pipeline and cannot tie the output to any recorded input. That split, base passing and step failing, is the signature of a window that is too short, and the engine chapter returns to it:
// formal: prove 2 expect unproven slang top pipe3
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
// Lesson-local parameter: BUG=1 makes the multiplier ignore bit 3 of the stage-1 copy of c.
module pipe3 #(parameter CHECK = 1, parameter BUG = 0) (
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 // stage-2 register, exposed for the miter's helper invariant
);
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] * ((BUG == 1) ? {1'b0, c1[2:0]} : c1);
y <= p + 8'd1;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history, as plain registers (works in every front 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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// after reset the output register is 0
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
endmodule
module pipe3_retimed #(parameter BUG = 0) (
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 [3:0] dbg_s2, // stage-2 registers, exposed for the miter's helper invariant
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
// helper invariant across the moved cut: the reference's stage-2 register p equals the
// twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmoduleThe check must also be able to fail. The mutant below makes the multiplier ignore bit 3 of the stage-1 copy of c, so the output is wrong whenever that bit is set. The bounded check one cycle too short passes, because a changed input needs four steps to reach the output; at depth 5 the latency check fails:
// formal: bmc 4 expect pass slang top pipe3 define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
// Lesson-local parameter: BUG=1 makes the multiplier ignore bit 3 of the stage-1 copy of c.
module pipe3 #(parameter CHECK = 1, parameter BUG = 0) (
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 // stage-2 register, exposed for the miter's helper invariant
);
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] * ((BUG == 1) ? {1'b0, c1[2:0]} : c1);
y <= p + 8'd1;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history, as plain registers (works in every front 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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// after reset the output register is 0
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
endmodule
module pipe3_retimed #(parameter BUG = 0) (
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 [3:0] dbg_s2, // stage-2 registers, exposed for the miter's helper invariant
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
// helper invariant across the moved cut: the reference's stage-2 register p equals the
// twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmodule// formal: bmc 5 expect fail slang top pipe3 define BUG=1
`define FORMAL
// pipe3: three-stage arithmetic pipeline, y = ((a + b)[3:0] * c[3:0]) + 1 (8 bits),
// registers: stage 1 {s = a + b, c1 = c[3:0]}, stage 2 {p = s[3:0] * c1}, stage 3 {y = p + 1}.
// Latency 3 cycles (y at cycle t+3 uses a, b, c of cycle t). Synchronous active-high
// reset clears every register. Only a[3:0], b[3:0], c[3:0] influence y.
// pipe3_retimed: same function and latency, registers moved across the multiplier:
// stage 1 {s, c1} (same), stage 2 {s2 = s[3:0], c2 = c1} (the multiplier moved to
// stage 3), stage 3 {y = s2 * c2 + 1}. BUG=1 injects a bug in the retimed twin: the
// multiplier ignores bit 3 of c2.
// pipe3_eq: miter of pipe3 against pipe3_retimed with common inputs; BUG is passed to the twin.
// Lesson-local parameter: BUG=1 makes the multiplier ignore bit 3 of the stage-1 copy of c.
module pipe3 #(parameter CHECK = 1, parameter BUG = 0) (
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 // stage-2 register, exposed for the miter's helper invariant
);
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] * ((BUG == 1) ? {1'b0, c1[2:0]} : c1);
y <= p + 8'd1;
end
end
`ifdef FORMAL
// CHECK=0 switches the properties off (used when pipe3 sits inside the miter)
generate if (CHECK) begin : g_chk
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// hist counts clean cycles since reset (saturates at 3): y is only specified after 3
reg [1:0] hist;
always @(posedge clk) begin
if (rst) hist <= 2'd0;
else if (hist != 2'd3) hist <= hist + 2'd1;
end
// input history, as plain registers (works in every front 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; // low 4 bits of a + b three cycles ago
// functional property with latency 3, checked only after 3 clean cycles
always @(*) if (!init && hist == 2'd3) a_latency3: assert (y == (sum3 * sc3) + 8'd1);
// after reset the output register is 0
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
endmodule
module pipe3_retimed #(parameter BUG = 0) (
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 [3:0] dbg_s2, // stage-2 registers, exposed for the miter's helper invariant
output wire [3:0] dbg_c2
);
reg [7:0] s;
reg [3:0] c1;
reg [3:0] s2, c2;
assign dbg_s2 = s2;
assign dbg_c2 = c2;
always @(posedge clk) begin
if (rst) begin s <= 8'd0; c1 <= 4'd0; s2 <= 4'd0; c2 <= 4'd0; y <= 8'd0; end
else begin
s <= a + b;
c1 <= c[3:0];
s2 <= s[3:0];
c2 <= c1;
y <= s2 * ((BUG == 1) ? {1'b0, c2[2:0]} : c2) + 8'd1;
end
end
endmodule
module pipe3_eq #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire [7:0] a,
input wire [7:0] b,
input wire [7:0] c,
output wire same
);
wire [7:0] y1, y2, p_ref;
wire [3:0] s2_ret, c2_ret;
pipe3 #(.CHECK(0)) u_ref (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y1), .dbg_p(p_ref));
pipe3_retimed #(.BUG(BUG)) u_ret (.clk(clk), .rst(rst), .a(a), .b(b), .c(c), .y(y2), .dbg_s2(s2_ret), .dbg_c2(c2_ret));
assign same = (y1 == y2);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_equiv: assert (same);
// helper invariant across the moved cut: the reference's stage-2 register p equals the
// twin's s2 * c2 (the multiplier result computed one stage later). Not needed if k >= 2.
generate if (HELPER) begin : g_helper
always @(*) if (!init) h_cut: assert (p_ref == s2_ret * c2_ret);
end endgenerate
always @(*) if (!init) c_nonzero: cover (y1 == 8'd7 && y2 == 8'd7);
`endif
endmoduleThe same compilation handles a range. The textbook sequence and the textbook response rule are shown for reading only:
// not-run: delay operators are not accepted by this front end
// textbook sequence: req ##[1:3] gnt // matches when gnt is high now and req was high 1, 2 or 3 cycles ago
// textbook response: req |-> ##[1:3] gnt // a request at t needs a grant in t+1, t+2 or t+3
// Boolean sequence: gnt && (req_d1 || req_d2 || req_d3)
// Boolean response: !req_d3 || gnt_d2 || gnt_d1 || gnt // judged at t+3, when the window closesThe module below delays the grant by LAT cycles after each request and checks the Boolean response form. LAT of 1 and 3 are the two edges of the window and both pass; LAT of 4 answers one cycle too late and LAT of 0 answers in the same cycle, before the window opens, and both fail:
// formal: bmc 10 expect pass slang top range_stage define LAT=1
`define FORMAL
// range_stage: a grant appears LAT cycles after every request (LAT 0 means the same cycle).
// p_range is the Boolean form of req |-> ##[1:3] gnt : three request-history bits, two grant-history
// bits and the grant now. Valid LAT values for the rule are 1, 2 and 3.
module range_stage #(parameter LAT = 2) (
input wire clk,
input wire rst,
input wire req,
output wire gnt
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
assign gnt = (LAT == 0) ? req : (LAT == 1) ? r1 : (LAT == 2) ? r2 : (LAT == 3) ? r3 : r4;
reg req_d1, req_d2, req_d3, gnt_d1, gnt_d2;
always @(posedge clk) begin
if (rst) begin req_d1 <= 1'b0; req_d2 <= 1'b0; req_d3 <= 1'b0; gnt_d1 <= 1'b0; gnt_d2 <= 1'b0; end
else begin
req_d1 <= req; req_d2 <= req_d1; req_d3 <= req_d2;
gnt_d1 <= gnt; gnt_d2 <= gnt_d1;
end
end
always @(*) if (!init) p_range: assert (!req_d3 || gnt_d2 || gnt_d1 || gnt);
endmodule// formal: bmc 10 expect pass slang top range_stage define LAT=3
`define FORMAL
// range_stage: a grant appears LAT cycles after every request (LAT 0 means the same cycle).
// p_range is the Boolean form of req |-> ##[1:3] gnt : three request-history bits, two grant-history
// bits and the grant now. Valid LAT values for the rule are 1, 2 and 3.
module range_stage #(parameter LAT = 2) (
input wire clk,
input wire rst,
input wire req,
output wire gnt
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
assign gnt = (LAT == 0) ? req : (LAT == 1) ? r1 : (LAT == 2) ? r2 : (LAT == 3) ? r3 : r4;
reg req_d1, req_d2, req_d3, gnt_d1, gnt_d2;
always @(posedge clk) begin
if (rst) begin req_d1 <= 1'b0; req_d2 <= 1'b0; req_d3 <= 1'b0; gnt_d1 <= 1'b0; gnt_d2 <= 1'b0; end
else begin
req_d1 <= req; req_d2 <= req_d1; req_d3 <= req_d2;
gnt_d1 <= gnt; gnt_d2 <= gnt_d1;
end
end
always @(*) if (!init) p_range: assert (!req_d3 || gnt_d2 || gnt_d1 || gnt);
endmodule// formal: bmc 10 expect fail slang top range_stage define LAT=4
`define FORMAL
// range_stage: a grant appears LAT cycles after every request (LAT 0 means the same cycle).
// p_range is the Boolean form of req |-> ##[1:3] gnt : three request-history bits, two grant-history
// bits and the grant now. Valid LAT values for the rule are 1, 2 and 3.
module range_stage #(parameter LAT = 2) (
input wire clk,
input wire rst,
input wire req,
output wire gnt
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
assign gnt = (LAT == 0) ? req : (LAT == 1) ? r1 : (LAT == 2) ? r2 : (LAT == 3) ? r3 : r4;
reg req_d1, req_d2, req_d3, gnt_d1, gnt_d2;
always @(posedge clk) begin
if (rst) begin req_d1 <= 1'b0; req_d2 <= 1'b0; req_d3 <= 1'b0; gnt_d1 <= 1'b0; gnt_d2 <= 1'b0; end
else begin
req_d1 <= req; req_d2 <= req_d1; req_d3 <= req_d2;
gnt_d1 <= gnt; gnt_d2 <= gnt_d1;
end
end
always @(*) if (!init) p_range: assert (!req_d3 || gnt_d2 || gnt_d1 || gnt);
endmodule// formal: bmc 10 expect fail slang top range_stage define LAT=0
`define FORMAL
// range_stage: a grant appears LAT cycles after every request (LAT 0 means the same cycle).
// p_range is the Boolean form of req |-> ##[1:3] gnt : three request-history bits, two grant-history
// bits and the grant now. Valid LAT values for the rule are 1, 2 and 3.
module range_stage #(parameter LAT = 2) (
input wire clk,
input wire rst,
input wire req,
output wire gnt
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!req);
reg r1, r2, r3, r4;
always @(posedge clk) begin
if (rst) begin r1 <= 1'b0; r2 <= 1'b0; r3 <= 1'b0; r4 <= 1'b0; end
else begin r1 <= req; r2 <= r1; r3 <= r2; r4 <= r3; end
end
assign gnt = (LAT == 0) ? req : (LAT == 1) ? r1 : (LAT == 2) ? r2 : (LAT == 3) ? r3 : r4;
reg req_d1, req_d2, req_d3, gnt_d1, gnt_d2;
always @(posedge clk) begin
if (rst) begin req_d1 <= 1'b0; req_d2 <= 1'b0; req_d3 <= 1'b0; gnt_d1 <= 1'b0; gnt_d2 <= 1'b0; end
else begin
req_d1 <= req; req_d2 <= req_d1; req_d3 <= req_d2;
gnt_d1 <= gnt; gnt_d2 <= gnt_d1;
end
end
always @(*) if (!init) p_range: assert (!req_d3 || gnt_d2 || gnt_d1 || gnt);
endmoduleThe history depth matches the pipeline latency exactly: three stages, three history registers, and the check fires only after three clean cycles.
Upper input bits that the design ignores are absent from the history: only the low nibbles travel through the registers.
A range rule is tested at both edges of its window: one cycle too early and one cycle too late must each fail.
Repetition bounds are counters with explicit resets, never bare delay chains whose length is hidden in the operator.
Count the history stages against the pipeline stages before running anything: a mismatch is visible on paper. Then run the proof at the full window and, as a sanity check, one window shorter: the shorter run must fail in the step while the base passes. If the full window fails in the base instead, the history wiring is wrong, not the window.
The base case starts from reset, where the pipeline is empty and consistent. The step starts from an arbitrary state, where two history stages cannot determine a three-stage output, so the step counterexample starts mid-pipeline. The failure is a short window, not a design bug.