A flawed property that passes is worse than no property: it certifies the bug. Each item below is a real answer shape seen in interviews, shown as written, with the defect, what the flaw does to the result, and a corrected runnable form with its failing partner. The corrections run as small lesson-local designs, so every repair is checked, not asserted.
Job of this lesson: find six defects and write corrections that run and can fail.
// not-run: implication operators and sequences are not accepted by this front end
// Flawed: assert property (@(posedge clk) req |=> ##[1:$] gnt);
// The unbounded window cannot fail on any finite prefix and no engine here
// checks lassos, so this never refutes a starved requester.Defect: an unbounded eventuality where a proof is needed. Effect: the property is uncheckable in this flow and a starvation hides behind it. Correction: a bounded response, a safety property with a derived window, checked with a wait counter. The grant here is registered, one cycle after the request, so a continuously requesting client waits at most 1 cycle and the bound is 1. The good design is proved; with the grant stuck at 0 the wait counter breaks the bound at step 3: depth 3 passes, depth 4 fails.
// formal: prove 6 expect pass slang top bounded_resp
`define FORMAL
// Lesson-local demo: registered grant, one cycle after the request; the wait counter is bounded by 1.
module bounded_resp #(parameter BUG = 0) (
input wire clk, input wire rst, input wire req, output reg gnt
);
always @(posedge clk) begin
if (rst) gnt <= 1'b0;
else gnt <= (BUG == 1) ? 1'b0 : req;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] w;
always @(posedge clk) begin
if (rst) w <= 2'd0;
else if (!req || gnt) w <= 2'd0;
else w <= w + 2'd1;
end
always @(*) if (!init) a_bounded: assert (w <= 2'd1);
`endif
endmodule// formal: bmc 3 expect pass slang top bounded_resp define BUG=1
`define FORMAL
// Lesson-local demo: registered grant, one cycle after the request; the wait counter is bounded by 1.
module bounded_resp #(parameter BUG = 0) (
input wire clk, input wire rst, input wire req, output reg gnt
);
always @(posedge clk) begin
if (rst) gnt <= 1'b0;
else gnt <= (BUG == 1) ? 1'b0 : req;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] w;
always @(posedge clk) begin
if (rst) w <= 2'd0;
else if (!req || gnt) w <= 2'd0;
else w <= w + 2'd1;
end
always @(*) if (!init) a_bounded: assert (w <= 2'd1);
`endif
endmodule// formal: bmc 4 expect fail slang top bounded_resp define BUG=1
`define FORMAL
// Lesson-local demo: registered grant, one cycle after the request; the wait counter is bounded by 1.
module bounded_resp #(parameter BUG = 0) (
input wire clk, input wire rst, input wire req, output reg gnt
);
always @(posedge clk) begin
if (rst) gnt <= 1'b0;
else gnt <= (BUG == 1) ? 1'b0 : req;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] w;
always @(posedge clk) begin
if (rst) w <= 2'd0;
else if (!req || gnt) w <= 2'd0;
else w <= w + 2'd1;
end
always @(*) if (!init) a_bounded: assert (w <= 2'd1);
`endif
endmodule// bad-example
// Flawed: assert (count |- DEPTH && count=0);
// Two defects in one line: |- where |-> belongs, and = where == belongs.Defect: a misspelled operator and an assignment inside the check. Effect: the line does not state overflow-freedom at all; depending on the front end it is rejected or parsed as something unintended. Correction: name the bound and the comparison explicitly. On a counter that wraps at 5, the overflow check is that the count never leaves 0 to 5. The good counter is proved; the variant that wraps at 6 reaches 6 at step 7: depth 7 passes, depth 8 fails.
// formal: prove 4 expect pass slang top mod6
`define FORMAL
// Lesson-local demo: mod-6 counter. BUG=1 wraps at 6; TAUT=1 swaps the real bound for one a 3-bit signal cannot violate.
module mod6 #(parameter BUG = 0, parameter TAUT = 0) (
input wire clk, input wire rst, input wire en, output reg [2:0] c
);
wire [2:0] last = (BUG == 1) ? 3'd6 : 3'd5;
always @(posedge clk) begin
if (rst) c <= 3'd0;
else if (en) c <= (c == last) ? 3'd0 : c + 3'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (TAUT == 1) begin : g_taut
always @(*) if (!init) a_range: assert (c <= 3'd7);
end else begin : g_real
always @(*) if (!init) a_range: assert (c <= 3'd5);
end endgenerate
`endif
endmodule// formal: bmc 7 expect pass slang top mod6 define BUG=1
`define FORMAL
// Lesson-local demo: mod-6 counter. BUG=1 wraps at 6; TAUT=1 swaps the real bound for one a 3-bit signal cannot violate.
module mod6 #(parameter BUG = 0, parameter TAUT = 0) (
input wire clk, input wire rst, input wire en, output reg [2:0] c
);
wire [2:0] last = (BUG == 1) ? 3'd6 : 3'd5;
always @(posedge clk) begin
if (rst) c <= 3'd0;
else if (en) c <= (c == last) ? 3'd0 : c + 3'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (TAUT == 1) begin : g_taut
always @(*) if (!init) a_range: assert (c <= 3'd7);
end else begin : g_real
always @(*) if (!init) a_range: assert (c <= 3'd5);
end endgenerate
`endif
endmodule// formal: bmc 8 expect fail slang top mod6 define BUG=1
`define FORMAL
// Lesson-local demo: mod-6 counter. BUG=1 wraps at 6; TAUT=1 swaps the real bound for one a 3-bit signal cannot violate.
module mod6 #(parameter BUG = 0, parameter TAUT = 0) (
input wire clk, input wire rst, input wire en, output reg [2:0] c
);
wire [2:0] last = (BUG == 1) ? 3'd6 : 3'd5;
always @(posedge clk) begin
if (rst) c <= 3'd0;
else if (en) c <= (c == last) ? 3'd0 : c + 3'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (TAUT == 1) begin : g_taut
always @(*) if (!init) a_range: assert (c <= 3'd7);
end else begin : g_real
always @(*) if (!init) a_range: assert (c <= 3'd5);
end endgenerate
`endif
endmodule// bad-example
// Flawed: assert property (@(posedge clk) strong(req) |-> ##[1:3] gnt);
// Strength belongs on the obligation, never on the trigger.Defect: a strong operator wrapped around the antecedent. Effect: it changes nothing about the obligation and shows a misunderstanding of where the demand sits. Correction: the demand is on the consequent. A bounded response is a safety property; written as a sequence it is weak unless the window is wrapped in strong, and the counter form of item 1 needs no such choice. No separate run is needed: the runnable shape is the same bounded response.
// bad-example
// Flawed: assert (gnt == $past(req, 1, 8));
// The third argument is a gating expression, not a window: this is just $past(req, 1).Defect: reading the gating argument as a look-back window. Effect: a one-cycle check filed as an eight-cycle check opens a seven-cycle hole. Correction: the plain one-cycle form where one cycle is meant, and a history shift register for within the last N. Below, the registered grant is checked against the previous request, and a 3-bit shift register drives a flag for a request in the last three cycles, checked against the three sampled-history reads. The mutant that drops the oldest bit passes until a request is exactly three cycles old: depth 5 passes, depth 6 fails.
// formal: prove 6 expect pass slang top hist_demo
`define FORMAL
// Lesson-local demo: registered grant checked against the previous request, and a 3-bit history register
// for "a request in the last three cycles"; BUG=1 drops the oldest bit.
module hist_demo #(parameter BUG = 0) (
input wire clk, input wire rst, input wire req, output reg gnt, output wire recent
);
reg [2:0] hist;
always @(posedge clk) begin
if (rst) begin gnt <= 1'b0; hist <= 3'b000; end
else begin
gnt <= req;
hist <= {hist[1:0], req};
end
end
assign recent = (BUG == 1) ? (hist[1] | hist[0]) : (hist[2] | hist[1] | hist[0]);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] age;
always @(posedge clk) begin
if (rst) age <= 2'd0;
else if (age != 2'd3) age <= age + 2'd1;
end
always @(posedge clk) if (!init && !$past(rst)) a_resp: assert (gnt == $past(req));
always @(posedge clk) if (!init && age == 2'd3) a_recent: assert (recent == ($past(req, 1) | $past(req, 2) | $past(req, 3)));
`endif
endmodule// formal: bmc 5 expect pass slang top hist_demo define BUG=1
`define FORMAL
// Lesson-local demo: registered grant checked against the previous request, and a 3-bit history register
// for "a request in the last three cycles"; BUG=1 drops the oldest bit.
module hist_demo #(parameter BUG = 0) (
input wire clk, input wire rst, input wire req, output reg gnt, output wire recent
);
reg [2:0] hist;
always @(posedge clk) begin
if (rst) begin gnt <= 1'b0; hist <= 3'b000; end
else begin
gnt <= req;
hist <= {hist[1:0], req};
end
end
assign recent = (BUG == 1) ? (hist[1] | hist[0]) : (hist[2] | hist[1] | hist[0]);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] age;
always @(posedge clk) begin
if (rst) age <= 2'd0;
else if (age != 2'd3) age <= age + 2'd1;
end
always @(posedge clk) if (!init && !$past(rst)) a_resp: assert (gnt == $past(req));
always @(posedge clk) if (!init && age == 2'd3) a_recent: assert (recent == ($past(req, 1) | $past(req, 2) | $past(req, 3)));
`endif
endmodule// formal: bmc 6 expect fail slang top hist_demo define BUG=1
`define FORMAL
// Lesson-local demo: registered grant checked against the previous request, and a 3-bit history register
// for "a request in the last three cycles"; BUG=1 drops the oldest bit.
module hist_demo #(parameter BUG = 0) (
input wire clk, input wire rst, input wire req, output reg gnt, output wire recent
);
reg [2:0] hist;
always @(posedge clk) begin
if (rst) begin gnt <= 1'b0; hist <= 3'b000; end
else begin
gnt <= req;
hist <= {hist[1:0], req};
end
end
assign recent = (BUG == 1) ? (hist[1] | hist[0]) : (hist[2] | hist[1] | hist[0]);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
reg [1:0] age;
always @(posedge clk) begin
if (rst) age <= 2'd0;
else if (age != 2'd3) age <= age + 2'd1;
end
always @(posedge clk) if (!init && !$past(rst)) a_resp: assert (gnt == $past(req));
always @(posedge clk) if (!init && age == 2'd3) a_recent: assert (recent == ($past(req, 1) | $past(req, 2) | $past(req, 3)));
`endif
endmodule// bad-example
// Flawed: assert (c3 == c3); // and its cousin assert (c3 <= 3'd7) on a 3-bit c3
// True by construction: proves nothing about the design.Defect: a bound the signal cannot violate, or a self-comparison. Effect: a passing check with zero protective value. Correction: bound the reachable behaviour the design must hold, here 0 to 5 on the mod-6 counter of item 2, and let a mutation run demonstrate it. The same wrap bug passes the tautological bound at depth 12 (the run below), while the real bound fails it at depth 8.
// formal: bmc 12 expect pass slang top mod6 define BUG=1 define TAUT=1
`define FORMAL
// Lesson-local demo: mod-6 counter. BUG=1 wraps at 6; TAUT=1 swaps the real bound for one a 3-bit signal cannot violate.
module mod6 #(parameter BUG = 0, parameter TAUT = 0) (
input wire clk, input wire rst, input wire en, output reg [2:0] c
);
wire [2:0] last = (BUG == 1) ? 3'd6 : 3'd5;
always @(posedge clk) begin
if (rst) c <= 3'd0;
else if (en) c <= (c == last) ? 3'd0 : c + 3'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (TAUT == 1) begin : g_taut
always @(*) if (!init) a_range: assert (c <= 3'd7);
end else begin : g_real
always @(*) if (!init) a_range: assert (c <= 3'd5);
end endgenerate
`endif
endmodule// not-run: this flow rejects the unknown-value system function (unsupported system task)
// Flawed: assert (!$isunknown(out));
// Two-state formal has no unknown value to find. Measured here: the front end that reads
// concurrent assertions rejects the call, and the other accepts it and reports a counterexample
// at a small depth on a flop whose value is plainly known, so neither result says anything about X.Defect: asking a two-state model about unknown values. Effect: no X question is answered while the report suggests coverage. Correction: a reset-determinism proof: the state after reset is independent of the free initial values. Below, two copies of a counter start from free values and are both reset to 0: they stay equal for ever. The failing partner leaves one copy unreset, and the equality fails at depth 2: depth 1 passes. One missing reset makes the post-reset state depend on the free start.
// formal: prove 4 expect pass slang top det_pair
`define FORMAL
// Lesson-local demo: reset determinism of two copies that start from free values; BUG=1 leaves one copy unreset.
module det_pair #(parameter BUG = 0) (
input wire clk, input wire rst, output wire same
);
reg [1:0] a, b;
always @(posedge clk) begin
if (rst) begin
a <= 2'd0;
if (BUG == 0) b <= 2'd0;
end else begin
a <= a + 2'd1;
b <= b + 2'd1;
end
end
assign same = (a == b);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_det: assert (same);
`endif
endmodule// formal: bmc 1 expect pass slang top det_pair define BUG=1
`define FORMAL
// Lesson-local demo: reset determinism of two copies that start from free values; BUG=1 leaves one copy unreset.
module det_pair #(parameter BUG = 0) (
input wire clk, input wire rst, output wire same
);
reg [1:0] a, b;
always @(posedge clk) begin
if (rst) begin
a <= 2'd0;
if (BUG == 0) b <= 2'd0;
end else begin
a <= a + 2'd1;
b <= b + 2'd1;
end
end
assign same = (a == b);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_det: assert (same);
`endif
endmodule// formal: bmc 2 expect fail slang top det_pair define BUG=1
`define FORMAL
// Lesson-local demo: reset determinism of two copies that start from free values; BUG=1 leaves one copy unreset.
module det_pair #(parameter BUG = 0) (
input wire clk, input wire rst, output wire same
);
reg [1:0] a, b;
always @(posedge clk) begin
if (rst) begin
a <= 2'd0;
if (BUG == 0) b <= 2'd0;
end else begin
a <= a + 2'd1;
b <= b + 2'd1;
end
end
assign same = (a == b);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_det: assert (same);
`endif
endmoduleIts failing partner: a correction that cannot fail is another tautology. Change the design or mutate the property until the buggy run fails at a stated step.