A registered output is checked in the same cycle as its input, and the proof fails on the good design. Or the reverse: a combinational output is checked a cycle late, and the proof fails on the good design there too. Both are the same error, the most common off-by-one in review, and this lesson's one job is to make the two offsets unconfusable.
Overlapped implication checks the consequent in the same cycle as the antecedent; non-overlapped checks it one cycle later. In Boolean history form the difference is exactly one history flop: compare against the current antecedent, or against the antecedent sampled last cycle. There is no third option and no middle cycle, which is why the review question is always which cycle the comparator looks at.
Every path has one right offset: a combinational path is due in the same cycle, a path through one register is due in the next. The wrong offset fails on the good design, which is annoying but safe. The dangerous case is a rule that passes on the good design and also on a mutant that answers a cycle off. So each offset needs its own mutant, and the mutant must fail the right form and only the right form.
A stage presents an accepted beat at its output either in the same cycle (a combinational path) or one cycle later (one register), mirroring the bridge's output path. The textbook pair reads clearly and does not run on this front end:
// not-run: implication operators are not accepted by this front end
// textbook pair on one accepted beat:
// in_valid |-> out_valid (same cycle, overlapped)
// in_valid |=> out_valid (next cycle, non-overlapped)
// the Boolean blocks below run each meaning as a one-way rule on the same stimulus:
// same cycle: !in_valid || (out_valid && out_data == in_data)
// next cycle: !$past(in_valid) || (out_valid && out_data == $past(in_data))The runnable pair is the same two meanings. The parameters choose the path latency LAT, the checked offset OFF, and whether the stage is mutated: BUG adds one register, so the mutant is always one cycle later than its good design. Start with the registered stage. The same-cycle form fails on the good design: the solver presents a beat, and the output is still low in that cycle because the register has not clocked it through yet. The next-cycle form passes on the same design:
// formal: bmc 8 expect fail slang top beat_pipe define LAT=1 define OFF=0
`define FORMAL
// beat_pipe: a stage that presents each input beat at its output LAT cycles later
// (LAT 1: one register, LAT 0: a combinational path). BUG=1 adds one more register,
// a mutant that answers a cycle late. OFF selects the checked offset: 0 means the same
// cycle as the beat (overlapped), 1 means the next cycle (non-overlapped). Both are
// written as one-way rules, the way the textbook implication reads: a beat implies its output.
module beat_pipe #(parameter LAT = 1, parameter BUG = 0, parameter OFF = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!in_valid);
reg v1, v2;
reg [7:0] d1, d2;
always @(posedge clk) begin
if (rst) begin v1 <= 1'b0; v2 <= 1'b0; d1 <= 8'd0; d2 <= 8'd0; end
else begin v1 <= in_valid; d1 <= in_data; v2 <= v1; d2 <= d1; end
end
localparam DEPTH = LAT + BUG;
assign out_valid = (DEPTH == 0) ? in_valid : (DEPTH == 1) ? v1 : v2;
assign out_data = (DEPTH == 0) ? in_data : (DEPTH == 1) ? d1 : d2;
always @(posedge clk) if (!init && !$past(rst)) begin
if (OFF == 0) p_same_cycle: assert (!in_valid || (out_valid && out_data == in_data));
else p_next_cycle: assert (!$past(in_valid) || (out_valid && out_data == $past(in_data)));
end
endmodule// formal: bmc 8 expect pass slang top beat_pipe define LAT=1 define OFF=1
`define FORMAL
// beat_pipe: a stage that presents each input beat at its output LAT cycles later
// (LAT 1: one register, LAT 0: a combinational path). BUG=1 adds one more register,
// a mutant that answers a cycle late. OFF selects the checked offset: 0 means the same
// cycle as the beat (overlapped), 1 means the next cycle (non-overlapped). Both are
// written as one-way rules, the way the textbook implication reads: a beat implies its output.
module beat_pipe #(parameter LAT = 1, parameter BUG = 0, parameter OFF = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!in_valid);
reg v1, v2;
reg [7:0] d1, d2;
always @(posedge clk) begin
if (rst) begin v1 <= 1'b0; v2 <= 1'b0; d1 <= 8'd0; d2 <= 8'd0; end
else begin v1 <= in_valid; d1 <= in_data; v2 <= v1; d2 <= d1; end
end
localparam DEPTH = LAT + BUG;
assign out_valid = (DEPTH == 0) ? in_valid : (DEPTH == 1) ? v1 : v2;
assign out_data = (DEPTH == 0) ? in_data : (DEPTH == 1) ? d1 : d2;
always @(posedge clk) if (!init && !$past(rst)) begin
if (OFF == 0) p_same_cycle: assert (!in_valid || (out_valid && out_data == in_data));
else p_next_cycle: assert (!$past(in_valid) || (out_valid && out_data == $past(in_data)));
end
endmoduleThe late mutant adds a second register. The next-cycle form catches it, because the beat now arrives two cycles after acceptance. The same-cycle form could not: it was already failing on the good design and so tells the good stage from the mutant nothing:
// formal: bmc 8 expect fail slang top beat_pipe define LAT=1 define BUG=1 define OFF=1
`define FORMAL
// beat_pipe: a stage that presents each input beat at its output LAT cycles later
// (LAT 1: one register, LAT 0: a combinational path). BUG=1 adds one more register,
// a mutant that answers a cycle late. OFF selects the checked offset: 0 means the same
// cycle as the beat (overlapped), 1 means the next cycle (non-overlapped). Both are
// written as one-way rules, the way the textbook implication reads: a beat implies its output.
module beat_pipe #(parameter LAT = 1, parameter BUG = 0, parameter OFF = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!in_valid);
reg v1, v2;
reg [7:0] d1, d2;
always @(posedge clk) begin
if (rst) begin v1 <= 1'b0; v2 <= 1'b0; d1 <= 8'd0; d2 <= 8'd0; end
else begin v1 <= in_valid; d1 <= in_data; v2 <= v1; d2 <= d1; end
end
localparam DEPTH = LAT + BUG;
assign out_valid = (DEPTH == 0) ? in_valid : (DEPTH == 1) ? v1 : v2;
assign out_data = (DEPTH == 0) ? in_data : (DEPTH == 1) ? d1 : d2;
always @(posedge clk) if (!init && !$past(rst)) begin
if (OFF == 0) p_same_cycle: assert (!in_valid || (out_valid && out_data == in_data));
else p_next_cycle: assert (!$past(in_valid) || (out_valid && out_data == $past(in_data)));
end
endmoduleNow the combinational path. Here the roles swap. The same-cycle form is the right one and passes on the good design; the registered mutant, one cycle late, fails it. The next-cycle form is the wrong one on this path and fails on the good design:
// formal: bmc 8 expect pass slang top beat_pipe define LAT=0 define OFF=0
`define FORMAL
// beat_pipe: a stage that presents each input beat at its output LAT cycles later
// (LAT 1: one register, LAT 0: a combinational path). BUG=1 adds one more register,
// a mutant that answers a cycle late. OFF selects the checked offset: 0 means the same
// cycle as the beat (overlapped), 1 means the next cycle (non-overlapped). Both are
// written as one-way rules, the way the textbook implication reads: a beat implies its output.
module beat_pipe #(parameter LAT = 1, parameter BUG = 0, parameter OFF = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!in_valid);
reg v1, v2;
reg [7:0] d1, d2;
always @(posedge clk) begin
if (rst) begin v1 <= 1'b0; v2 <= 1'b0; d1 <= 8'd0; d2 <= 8'd0; end
else begin v1 <= in_valid; d1 <= in_data; v2 <= v1; d2 <= d1; end
end
localparam DEPTH = LAT + BUG;
assign out_valid = (DEPTH == 0) ? in_valid : (DEPTH == 1) ? v1 : v2;
assign out_data = (DEPTH == 0) ? in_data : (DEPTH == 1) ? d1 : d2;
always @(posedge clk) if (!init && !$past(rst)) begin
if (OFF == 0) p_same_cycle: assert (!in_valid || (out_valid && out_data == in_data));
else p_next_cycle: assert (!$past(in_valid) || (out_valid && out_data == $past(in_data)));
end
endmodule// formal: bmc 8 expect fail slang top beat_pipe define LAT=0 define BUG=1 define OFF=0
`define FORMAL
// beat_pipe: a stage that presents each input beat at its output LAT cycles later
// (LAT 1: one register, LAT 0: a combinational path). BUG=1 adds one more register,
// a mutant that answers a cycle late. OFF selects the checked offset: 0 means the same
// cycle as the beat (overlapped), 1 means the next cycle (non-overlapped). Both are
// written as one-way rules, the way the textbook implication reads: a beat implies its output.
module beat_pipe #(parameter LAT = 1, parameter BUG = 0, parameter OFF = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!in_valid);
reg v1, v2;
reg [7:0] d1, d2;
always @(posedge clk) begin
if (rst) begin v1 <= 1'b0; v2 <= 1'b0; d1 <= 8'd0; d2 <= 8'd0; end
else begin v1 <= in_valid; d1 <= in_data; v2 <= v1; d2 <= d1; end
end
localparam DEPTH = LAT + BUG;
assign out_valid = (DEPTH == 0) ? in_valid : (DEPTH == 1) ? v1 : v2;
assign out_data = (DEPTH == 0) ? in_data : (DEPTH == 1) ? d1 : d2;
always @(posedge clk) if (!init && !$past(rst)) begin
if (OFF == 0) p_same_cycle: assert (!in_valid || (out_valid && out_data == in_data));
else p_next_cycle: assert (!$past(in_valid) || (out_valid && out_data == $past(in_data)));
end
endmodule// formal: bmc 8 expect fail slang top beat_pipe define LAT=0 define OFF=1
`define FORMAL
// beat_pipe: a stage that presents each input beat at its output LAT cycles later
// (LAT 1: one register, LAT 0: a combinational path). BUG=1 adds one more register,
// a mutant that answers a cycle late. OFF selects the checked offset: 0 means the same
// cycle as the beat (overlapped), 1 means the next cycle (non-overlapped). Both are
// written as one-way rules, the way the textbook implication reads: a beat implies its output.
module beat_pipe #(parameter LAT = 1, parameter BUG = 0, parameter OFF = 1) (
input wire clk,
input wire rst,
input wire in_valid,
input wire [7:0] in_data,
output wire out_valid,
output wire [7:0] out_data
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!in_valid);
reg v1, v2;
reg [7:0] d1, d2;
always @(posedge clk) begin
if (rst) begin v1 <= 1'b0; v2 <= 1'b0; d1 <= 8'd0; d2 <= 8'd0; end
else begin v1 <= in_valid; d1 <= in_data; v2 <= v1; d2 <= d1; end
end
localparam DEPTH = LAT + BUG;
assign out_valid = (DEPTH == 0) ? in_valid : (DEPTH == 1) ? v1 : v2;
assign out_data = (DEPTH == 0) ? in_data : (DEPTH == 1) ? d1 : d2;
always @(posedge clk) if (!init && !$past(rst)) begin
if (OFF == 0) p_same_cycle: assert (!in_valid || (out_valid && out_data == in_data));
else p_next_cycle: assert (!$past(in_valid) || (out_valid && out_data == $past(in_data)));
end
endmodulePath | Form checked | Good design | One-cycle-late mutant |
|---|---|---|---|
Registered (LAT 1) | Same cycle | Counterexample (wrong offset) | Not run: it already fails the good design. |
Registered (LAT 1) | Next cycle | No counterexample to depth 8 | Counterexample. |
Combinational (LAT 0) | Same cycle | No counterexample to depth 8 | Counterexample. |
Combinational (LAT 0) | Next cycle | Counterexample (wrong offset) | Not run: it already fails the good design. |
How to read it: one slot is one step, counted from the first step after reset, so slot 1 is step 1. in_valid carries one beat, in step 2. ov_comb, the output of the combinational path, is high in step 2; ov_reg, the output through one register, is high in step 3; ov_late, the output through two registers, is high in step 4. Each lane named same_ok or next_ok is high while that form holds and drops in the step where the form is violated. On the combinational path the same-cycle form, same_ok_comb, stays high in every step, and the next-cycle form, next_ok_comb, drops in step 3, where the output has already gone. On the one-register stage the same-cycle form, same_ok_reg, drops in step 2, where the beat is on the input and the output is still low, and the next-cycle form, next_ok_reg, stays high in every step. The two-register stage fails the next-cycle form: next_ok_late drops in step 3, because the output is still low one step after the beat.
The right form is the one whose good-design cell is clean, and only that form has a mutant cell worth reading. The runnable forms are one-way, like the textbook implication: a beat must appear, but nothing forbids other outputs.
The property comment states the due cycle in words: same cycle for a combinational path, next cycle for one register, never just the operator.
Data travels with its valid through the same history depth: the data comparison uses the same sampled cycle as the valid comparison.
Each offset has its mutant test: the right form fails a design that is one register too slow, and the other offset is shown failing the good design so nobody adopts it by accident.
Run both offsets on every new rule: exactly one must pass on the good design, which tells you the path latency, and that form must fail on the mutant. If both pass, the rule is too weak to see the offset; if both fail, the antecedent is misaligned.
The rule cannot see the offset: it is too weak, or its antecedent never fires. Strengthen the consequent or check the antecedent cover before trusting the pass.