The dashboard says every assertion on a small counter block is proven in under a second. The cover report, on a side page nobody opened, says the activity cover was never reached. In the lab the block miscounts under back-to-back enables, and nobody saw it because the harness never let the enable assert.
Job of this lesson: run the harness variants side by side: a clean one, three over-constrained ones that pass for no reason, and the repair with its mutation evidence.
Trap | What the candidate does | Why it fails |
|---|---|---|
Silence a counterexample with an assumption | Each false trace gets a new rule. | The rules accumulate until the interesting behaviour is gone; a good proof needs fewer assumptions, each discharged. |
Trust the assertion column | Reports proven without opening the covers. | A vacuous pass is the fastest result the tool produces; speed without reached covers is suspicion, not evidence. |
Treat unreached covers as noise | Leaves the cover column unread. | An unreached cover on a required scenario fails signoff: each has an owner and a repair. |
An assumption removes behaviour; a cover shows that behaviour remains. The assertion column says nothing broke in what was checked; the cover column says something worth checking was exercised. A cover not reached within a depth is inconclusive on its own: it becomes a finding only when the assumption list shows why. So interrogate the harness before the design: list every assumption, remove those without an owner, and watch the covers return. Three harness faults empty the behaviour set: an assumption pinning the very signal under test, two rules pinning one signal to opposite values, and a reset held for ever.
The design is a 2-bit counter that steps on every enable. The bug variant sticks instead of stepping. Run A is the clean harness on the good design: the step property holds, including the wrap from 3 to 0, and the cover for the count reaching 2 is reached.
// formal: bmc 6 expect pass slang top ovc
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmodule// formal: cover 6 expect reached slang top ovc
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmoduleRun B adds one innocent-looking assumption, enable never asserted, to the buggy design. The step property passes because its antecedent needs a past enable that never comes. Only the cover column shows it: not reached within 6, inconclusive on its own, but here the assumption list explains it, since enable never asserted means the count can never reach 2.
// formal: bmc 6 expect pass slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) assume (!en);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmodule// formal: cover 6 expect fail slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) assume (!en);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmoduleRun C removes the assumption and reruns the buggy design. The stuck counter now fails the step property: depth 3 still passes and depth 4 fails, so the failing step is 3 (the property reads the previous cycle, so it reports a step after the stuck cycle). This is the mutation evidence the repaired harness must show.
// formal: bmc 3 expect pass slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmodule// formal: bmc 4 expect fail slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmoduleRuns D and E are the other two faults, both on the buggy design. D adds a contradictory pair, enable assumed high and enable assumed low: no behaviour satisfies both, so every assertion passes and every cover is unreached. E assumes reset for ever instead of for the first step: the design never leaves reset, the history guard never lets the step property fire, and the cover is unreached.
// formal: bmc 6 expect pass slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) assume (en);
always @(*) assume (!en);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmodule// formal: cover 6 expect fail slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) assume (en);
always @(*) assume (!en);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmodule// formal: bmc 6 expect pass slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmodule// formal: cover 6 expect fail slang top ovc define BUG=1
`define FORMAL
// Lesson-local demo: 2-bit enable counter with a stuck-when-enabled bug variant.
module ovc #(parameter BUG = 0) (
input wire clk, input wire rst, input wire en, output reg [1:0] c
);
always @(posedge clk) begin
if (rst) c <= 2'd0;
else if (en) c <= (BUG == 1) ? c : c + 2'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) assume (rst);
always @(posedge clk) if (!init && !$past(rst)) begin
a_count: assert (!$past(en) || c == $past(c) + 2'd1);
end
always @(*) if (!init) c_two: cover (c == 2'd2);
`endif
endmoduleRoot cause: an assumption hid the bug, and the unread cover column hid the assumption. Fix: assert what the block owes, assume only documented input rules, require every required cover reached, and keep one injected bug per property class that the harness demonstrably catches.
Assumptions are priced by the input space they remove. A 4-bit opcode restricted to 11 of 16 values plus a word-alignment rule on the address removes over four fifths of the space, and a bug living in the removed part is invisible by construction. Each excluded class needs a named verification home (figures illustrative).
def remaining(opcodes_kept, opcodes_all, address_fraction):
return (opcodes_kept / opcodes_all) * address_fraction
left = remaining(11, 16, 1 / 4)
assert abs(left - 11 / 64) < 1e-12, left
excluded = 1 - left
assert abs(excluded - 53 / 64) < 1e-12, excluded
assert excluded > 0.8, excluded
# The failing variant: the same call without the alignment rule understates the exclusion.
try:
assert abs(remaining(11, 16, 1) - left) < 1e-12
raise SystemExit("priced the opcode rule but dropped the alignment rule")
except AssertionError:
pass
print("PASS: 11/64 of the input space remains, 82.8 percent excluded by two rules")A strong answer opens the cover report before defending any proof, reads the assumption list aloud with an owner for each line, and names the run that separates the repaired harness from the false pass: the injected bug failing at a stated step. It closes with the signoff wording: proven for the stated model and assumptions, covers reached with steps, mutation evidence attached, excluded classes named with their verification home.
Dimension | Strong (3 to 4) | Weak (0 to 2) |
|---|---|---|
Assumption | Every assume listed, owned, discharged at a neighbour. | Assumptions undescribed; the enable rule unmentioned. |
Mechanism | Vacuity explained at cycle level: antecedent never fires. | Proven means correct. |
Trade-off | Fewer, documented assumptions versus quick convergence. | More assumptions to make it pass. |
Evidence | Cover steps plus the injected bug failing at step 3. | The passing report alone. |
Open the cover column: the repaired harness reaches its activity covers at stated steps and fails its injected bug; the false pass shows unreached covers and has no failing partner.