These six test judgement. Each keeps the four-part shape and names the trap that marks a memorised answer.
Assumption: the model the trace came from: reset, assumptions, bound. Mechanism: read from the first cycle, in order: is the start state legal; do the inputs obey every assumption (if not, the harness is at fault); does the failing cycle break a requirement or only a helper; does it replay on the unabstracted design (if not, an abstraction artefact). Trade-off: repairing the wrong side either ships the bug or hides it. Evidence: the classified trace, root cause, fix, a new cover and assertion. Trap: starting at the failing cycle. See triage a counterexample.
Assumption: the property concerns one address at a time and the control never branches on data. Mechanism: tracked-entry abstraction: one symbolic address, one shadow value, one valid bit, 8 plus 32 plus 1 is 41 bits instead of 8192. Trade-off: the full memory proves every address and never converges; the tracked entry converges for one-address properties only. Evidence: the bit count, covers showing the tracked address written then read, the data-independence argument. Trap: an address not constrained to the map. See memory and tracked entry abstraction.
import math
def tracked_bits(entries, width, valid=1):
return math.ceil(math.log2(entries)) + width + valid
full_bits = 256 * 32
assert full_bits == 8192, full_bits
assert tracked_bits(256, 32) == 41, tracked_bits(256, 32)
assert full_bits // tracked_bits(256, 32) >= 199
# The failing variant: the same call without the valid bit undercounts the harness state.
try:
assert tracked_bits(256, 32, valid=0) == 41
raise SystemExit("accepted a bit count without the valid bit")
except AssertionError:
pass
print("PASS: 8192 bits abstracted to 41 bits, about a 200 times reduction")Assumption: synchronous active-high reset, re-assertable. Mechanism: two gates hide two different things. The gate disable iff (rst) stops the check judging an output wrong only while reset is asserted. Below, vld is driven high by reset (BUG 1) though the flag was never set: the gated check passes prove 3 on the buggy design; the ungated check fails at depth 3 (depth 2 passes: a clocked check reports a step late) and passes the good design.
// formal: prove 3 expect pass slang top gate_hides
`define FORMAL
// Lesson-local demo: a valid flag driven high while reset is asserted (BUG=1); GATED=1 adds the reset gate.
module gate_hides #(parameter BUG = 1, parameter GATED = 1) (
input wire clk, input wire rst, input wire push, output wire vld
);
reg v;
always @(posedge clk) v <= rst ? 1'b0 : (v | push);
assign vld = v | (BUG == 1 && rst);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (GATED == 1) begin : g_gated
a_gated: assert property (@(posedge clk) disable iff (rst || init) !vld || v);
end else begin : g_open
a_open: assert property (@(posedge clk) disable iff (init) !vld || v);
end endgenerate
`endif
endmodule// formal: bmc 2 expect pass slang top gate_hides define GATED=0
`define FORMAL
// Lesson-local demo: a valid flag driven high while reset is asserted (BUG=1); GATED=1 adds the reset gate.
module gate_hides #(parameter BUG = 1, parameter GATED = 1) (
input wire clk, input wire rst, input wire push, output wire vld
);
reg v;
always @(posedge clk) v <= rst ? 1'b0 : (v | push);
assign vld = v | (BUG == 1 && rst);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (GATED == 1) begin : g_gated
a_gated: assert property (@(posedge clk) disable iff (rst || init) !vld || v);
end else begin : g_open
a_open: assert property (@(posedge clk) disable iff (init) !vld || v);
end endgenerate
`endif
endmodule// formal: bmc 3 expect fail slang top gate_hides define GATED=0
`define FORMAL
// Lesson-local demo: a valid flag driven high while reset is asserted (BUG=1); GATED=1 adds the reset gate.
module gate_hides #(parameter BUG = 1, parameter GATED = 1) (
input wire clk, input wire rst, input wire push, output wire vld
);
reg v;
always @(posedge clk) v <= rst ? 1'b0 : (v | push);
assign vld = v | (BUG == 1 && rst);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (GATED == 1) begin : g_gated
a_gated: assert property (@(posedge clk) disable iff (rst || init) !vld || v);
end else begin : g_open
a_open: assert property (@(posedge clk) disable iff (init) !vld || v);
end endgenerate
`endif
endmodule// formal: prove 3 expect pass slang top gate_hides define GATED=0 define BUG=0
`define FORMAL
// Lesson-local demo: a valid flag driven high while reset is asserted (BUG=1); GATED=1 adds the reset gate.
module gate_hides #(parameter BUG = 1, parameter GATED = 1) (
input wire clk, input wire rst, input wire push, output wire vld
);
reg v;
always @(posedge clk) v <= rst ? 1'b0 : (v | push);
assign vld = v | (BUG == 1 && rst);
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
generate if (GATED == 1) begin : g_gated
a_gated: assert property (@(posedge clk) disable iff (rst || init) !vld || v);
end else begin : g_open
a_open: assert property (@(posedge clk) disable iff (init) !vld || v);
end endgenerate
`endif
endmoduleThe history guard !$past(rst) skips the cycle after reset too. Reset sets q to 1 by mistake and run mode clears it next cycle: with the guard prove 3 passes on the buggy design, the guard skipping exactly the wrong cycle. The explicit reset-value check fails at depth 3 (depth 2 passes) and passes the good design to depth 5.
// formal: prove 3 expect pass slang top reset_skipped
`define FORMAL
// Lesson-local demo: a wrong reset value (1) that run-mode logic overwrites on the next cycle.
module reset_skipped #(parameter BUG = 1) (
input wire clk, input wire rst, output reg q
);
always @(posedge clk) begin
if (rst) q <= (BUG == 1) ? 1'b1 : 1'b0;
else q <= 1'b0;
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)) a_run: assert (q == 1'b0);
`endif
endmodule// formal: bmc 2 expect pass slang top reset_checked
`define FORMAL
// Lesson-local demo: the same design, with the cycle after reset checked explicitly.
module reset_checked #(parameter BUG = 1) (
input wire clk, input wire rst, output reg q
);
always @(posedge clk) begin
if (rst) q <= (BUG == 1) ? 1'b1 : 1'b0;
else q <= 1'b0;
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)) a_reset_val: assert (q == 1'b0);
`endif
endmodule// formal: bmc 3 expect fail slang top reset_checked
`define FORMAL
// Lesson-local demo: the same design, with the cycle after reset checked explicitly.
module reset_checked #(parameter BUG = 1) (
input wire clk, input wire rst, output reg q
);
always @(posedge clk) begin
if (rst) q <= (BUG == 1) ? 1'b1 : 1'b0;
else q <= 1'b0;
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)) a_reset_val: assert (q == 1'b0);
`endif
endmodule// formal: bmc 5 expect pass slang top reset_checked define BUG=0
`define FORMAL
// Lesson-local demo: the same design, with the cycle after reset checked explicitly.
module reset_checked #(parameter BUG = 1) (
input wire clk, input wire rst, output reg q
);
always @(posedge clk) begin
if (rst) q <= (BUG == 1) ? 1'b1 : 1'b0;
else q <= 1'b0;
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)) a_reset_val: assert (q == 1'b0);
`endif
endmoduleTrade-off: gating is cheap; an explicit reset-state check costs one property per reset-valued output. Evidence: one bug passing under each gate and failing under the explicit check. Trap: believing a gated pass covers reset. See asynchronous reset and disable iff.
Assumption: common inputs and reset, comparison after a defined point, modes enumerated. Mechanism: a miter feeds both implementations the same inputs and asserts equal outputs; twins that differ in timing need the latency window (how many cycles apart outputs may be) stated, retimed state needs its correspondence as a helper. Trade-off: one miter over all modes proves little about each; per-mode miters cost runs. Evidence: the passing miter, the injected bug's counterexample, the intended-difference property. Trap: claiming equivalence proves correctness. See two implementations of the arbiter and the ECO scenario.
Assumption: name the obligation first. Mechanism: formal wins on control, protocols, connectivity, arbiters, FIFOs and register maps: small cones, exact answers. It loses on deep arithmetic and long system flows, where the cone is everything. Trade-off: simulation covers long stories cheaply and approximately; formal covers every sequence of a small model exactly. Evidence: cone size per property and the bound justification. Trap: a tool preference instead of an obligation split. See the formal engineer's split.
Assumption: the RTL revision is frozen and named. Mechanism: every property proven or bounded with a justification; required covers reached; assumptions discharged; cone coverage; mutation results; a rerun on the final hash; waivers with reasons. Trade-off: a waiver ships known risk with an owner; demanding full proofs everywhere has no end. Evidence: the ledger, one row per property: outcome, depth or proof form, covers, assumptions. Trap: counting not-failed as proven. See the signoff checklist in full.
Never overrule a counterexample on its own model: it always wins. Overrule the model only, by naming the assumption, reset or abstraction that differed, fixing it and rerunning.