An engineer writes a history call with three arguments expecting a window, and the proof checks one cycle. Or writes a bare implication for a request-response pair and the proof passes on a design that answers twice. Both errors compile, both prove quickly, and both check less than the author believes. This lesson's one job is the two replacements: history registers for windows, counters for one-to-one.
The third argument of the sampled-value function is a gating expression, not a window: it says when the sampling is valid, not how far back to look. A call that looks like it reaches back eight cycles reaches back exactly one. A window over the last N cycles is N history bits ORed together, built by hand as registers. And one request with one response is not an implication at all: a bare implication is satisfied by the first answer and blind to the second, so the check counts outstanding requests in a register and bounds it.
The wrong window, written plainly so it is never copied:
// bad-example: the third argument is a gating expression, not a window;
// $past(req_accepted, 1, 8) reads as $past(req_accepted, 1): the 8 changes nothing,
// so the check below still looks exactly one cycle back
// w_wrong_window: assert property (@(posedge clk) !resp || $past(req_accepted, 1, 8));The front end used in this course refuses the three-argument call with an error, so the wrong window cannot be run as written. Its honest runnable equivalent is the one-argument call, which is what the three-argument form means anyway.
The rule is: every response must be preceded by an accepted request within the last three cycles. The module below delays its response by LAT cycles after the accept, and LAT of 2 is legal. The wrong window looks back exactly one cycle and fails on the legal slow response. The right window ORs three history bits and passes:
// formal: bmc 8 expect fail slang top window_resp define LAT=2 define WHICH=0
`define FORMAL
// window_resp: a response appears LAT cycles after every accept (LAT 1 to 3 is legal).
// WHICH=0 checks the response against $past(acc, 1): the one-cycle reading of the three-argument call.
// WHICH=1 checks it against the last three cycles: acc_d1 || acc_d2 || acc_d3.
module window_resp #(parameter LAT = 2, parameter WHICH = 0) (
input wire clk,
input wire rst,
input wire acc,
output wire resp
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!acc);
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 <= acc; r2 <= r1; r3 <= r2; r4 <= r3; end
end
assign resp = (LAT == 1) ? r1 : (LAT == 2) ? r2 : (LAT == 3) ? r3 : r4;
reg a1, a2, a3;
always @(posedge clk) begin
if (rst) begin a1 <= 1'b0; a2 <= 1'b0; a3 <= 1'b0; end
else begin a1 <= acc; a2 <= a1; a3 <= a2; end
end
generate if (WHICH == 0) begin : g_wrong
p_wrong: assert property (@(posedge clk) disable iff (init || rst) !resp || $past(acc, 1));
end else begin : g_right
p_right: assert property (@(posedge clk) disable iff (init || rst) !resp || a1 || a2 || a3);
end endgenerate
endmodule// formal: bmc 8 expect pass slang top window_resp define LAT=2 define WHICH=1
`define FORMAL
// window_resp: a response appears LAT cycles after every accept (LAT 1 to 3 is legal).
// WHICH=0 checks the response against $past(acc, 1): the one-cycle reading of the three-argument call.
// WHICH=1 checks it against the last three cycles: acc_d1 || acc_d2 || acc_d3.
module window_resp #(parameter LAT = 2, parameter WHICH = 0) (
input wire clk,
input wire rst,
input wire acc,
output wire resp
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!acc);
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 <= acc; r2 <= r1; r3 <= r2; r4 <= r3; end
end
assign resp = (LAT == 1) ? r1 : (LAT == 2) ? r2 : (LAT == 3) ? r3 : r4;
reg a1, a2, a3;
always @(posedge clk) begin
if (rst) begin a1 <= 1'b0; a2 <= 1'b0; a3 <= 1'b0; end
else begin a1 <= acc; a2 <= a1; a3 <= a2; end
end
generate if (WHICH == 0) begin : g_wrong
p_wrong: assert property (@(posedge clk) disable iff (init || rst) !resp || $past(acc, 1));
end else begin : g_right
p_right: assert property (@(posedge clk) disable iff (init || rst) !resp || a1 || a2 || a3);
end endgenerate
endmoduleBoth edges of the window must be tested. A response four cycles after the accept is outside the window and the right form fails it, so the OR is neither too short nor too long:
// formal: bmc 8 expect fail slang top window_resp define LAT=4 define WHICH=1
`define FORMAL
// window_resp: a response appears LAT cycles after every accept (LAT 1 to 3 is legal).
// WHICH=0 checks the response against $past(acc, 1): the one-cycle reading of the three-argument call.
// WHICH=1 checks it against the last three cycles: acc_d1 || acc_d2 || acc_d3.
module window_resp #(parameter LAT = 2, parameter WHICH = 0) (
input wire clk,
input wire rst,
input wire acc,
output wire resp
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!acc);
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 <= acc; r2 <= r1; r3 <= r2; r4 <= r3; end
end
assign resp = (LAT == 1) ? r1 : (LAT == 2) ? r2 : (LAT == 3) ? r3 : r4;
reg a1, a2, a3;
always @(posedge clk) begin
if (rst) begin a1 <= 1'b0; a2 <= 1'b0; a3 <= 1'b0; end
else begin a1 <= acc; a2 <= a1; a3 <= a2; end
end
generate if (WHICH == 0) begin : g_wrong
p_wrong: assert property (@(posedge clk) disable iff (init || rst) !resp || $past(acc, 1));
end else begin : g_right
p_right: assert property (@(posedge clk) disable iff (init || rst) !resp || a1 || a2 || a3);
end endgenerate
endmoduleThe stage below accepts words and answers each one two cycles later: the response is registered twice, so a response appears two cycles after its accept, and at most two accepts are outstanding. The bare implication demands a response two cycles after every accept. It is satisfied by the real answer and never looks for a second, so it passes on the mutant that emits a phantom duplicate. The outstanding counter, accepts minus responses, sees the duplicate: it would go below zero, which in three bits wraps to a large value that breaks the bound of two. On the good stage both properties pass:
// formal: bmc 8 expect pass slang define PROP=0
`define FORMAL
// accept_once: every accept is answered exactly once, two cycles later (resp is registered twice).
// BUG=1 emits a phantom second response one cycle after the real one.
// PROP selects the checks: 0 both, 1 the bare implication only, 2 the outstanding counter only.
// p_bare is acc |-> ##2 resp in Boolean form; p_one2one bounds accepts minus responses.
module accept_once #(parameter BUG = 0, parameter PROP = 0) (
input wire clk,
input wire rst,
input wire acc,
output reg resp,
output reg [2:0] bal
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!acc);
reg acc_d1, acc_d2;
always @(posedge clk) begin
if (rst) begin acc_d1 <= 1'b0; acc_d2 <= 1'b0; resp <= 1'b0; bal <= 3'd0; end
else begin
acc_d1 <= acc; acc_d2 <= acc_d1;
resp <= acc_d1 || (BUG == 1 && acc_d2);
bal <= bal + {2'b0, acc} - {2'b0, resp};
end
end
always @(posedge clk) if (!init && !$past(rst)) begin
if (PROP != 2) p_bare: assert (!acc_d2 || resp);
if (PROP != 1) p_one2one: assert (bal <= 3'd2);
end
endmoduleOn the mutant the bare implication alone still passes: the real answer satisfies it and the phantom is invisible to it. This is the claim of the lesson, shown by a run:
// formal: bmc 8 expect pass slang define BUG=1 define PROP=1
`define FORMAL
// accept_once: every accept is answered exactly once, two cycles later (resp is registered twice).
// BUG=1 emits a phantom second response one cycle after the real one.
// PROP selects the checks: 0 both, 1 the bare implication only, 2 the outstanding counter only.
// p_bare is acc |-> ##2 resp in Boolean form; p_one2one bounds accepts minus responses.
module accept_once #(parameter BUG = 0, parameter PROP = 0) (
input wire clk,
input wire rst,
input wire acc,
output reg resp,
output reg [2:0] bal
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!acc);
reg acc_d1, acc_d2;
always @(posedge clk) begin
if (rst) begin acc_d1 <= 1'b0; acc_d2 <= 1'b0; resp <= 1'b0; bal <= 3'd0; end
else begin
acc_d1 <= acc; acc_d2 <= acc_d1;
resp <= acc_d1 || (BUG == 1 && acc_d2);
bal <= bal + {2'b0, acc} - {2'b0, resp};
end
end
always @(posedge clk) if (!init && !$past(rst)) begin
if (PROP != 2) p_bare: assert (!acc_d2 || resp);
if (PROP != 1) p_one2one: assert (bal <= 3'd2);
end
endmoduleThe counter alone fails on the same mutant. Together the three runs are the whole argument: same design, same stimulus space, two properties, and only one of them can see a duplicate:
// formal: bmc 8 expect fail slang define BUG=1 define PROP=2
`define FORMAL
// accept_once: every accept is answered exactly once, two cycles later (resp is registered twice).
// BUG=1 emits a phantom second response one cycle after the real one.
// PROP selects the checks: 0 both, 1 the bare implication only, 2 the outstanding counter only.
// p_bare is acc |-> ##2 resp in Boolean form; p_one2one bounds accepts minus responses.
module accept_once #(parameter BUG = 0, parameter PROP = 0) (
input wire clk,
input wire rst,
input wire acc,
output reg resp,
output reg [2:0] bal
);
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (rst) assume (!acc);
reg acc_d1, acc_d2;
always @(posedge clk) begin
if (rst) begin acc_d1 <= 1'b0; acc_d2 <= 1'b0; resp <= 1'b0; bal <= 3'd0; end
else begin
acc_d1 <= acc; acc_d2 <= acc_d1;
resp <= acc_d1 || (BUG == 1 && acc_d2);
bal <= bal + {2'b0, acc} - {2'b0, resp};
end
end
always @(posedge clk) if (!init && !$past(rst)) begin
if (PROP != 2) p_bare: assert (!acc_d2 || resp);
if (PROP != 1) p_one2one: assert (bal <= 3'd2);
end
endmoduleDesign | Bare implication | Outstanding counter |
|---|---|---|
Good stage | No counterexample to depth 8 | No counterexample to depth 8 |
Phantom duplicate (BUG=1) | No counterexample to depth 8: blind | Counterexample |
No three-argument history call is read as a window: the review asks what the gating expression gates, and where the history register is.
Every request-response rule counts: an outstanding counter or a tracked item, never a bare implication alone.
The counter bound matches the design's buffering: here two outstanding accepts, the response latency, with the reset and wrap behaviour stated. A bound of one would fail the good stage on back-to-back accepts.
A window is tested at both edges: a response one cycle inside and one cycle outside the window must give different results.
Test every one-to-one rule against a duplicate: add the phantom response and confirm the rule fails. If it passes, the rule checks existence, not uniqueness, and a whole class of duplication bugs is invisible. For windows, test both edges: an answer one cycle too early and one cycle too late must each fail exactly one side of the OR.
It gates the sampling: it says in which cycles the sampled value may be used. The reach-back is set by the second argument, almost always one, and anything wider needs explicit history registers.