Two runs disagree: one passes, one fails, and the room divides over which to believe. The rule is short. On the same model, the same assumptions and the same reset, a counterexample always wins: no second run can prove that property, because the trace exists. Apparent conflicts always mean something differed: the bound, an assumption, the reset model, the design revision, or a tool defect. This lesson shows the cheapest version of the argument, depth, on the decade counter.
A formal run has exactly three outcomes. Proven means the property holds for the stated model under the stated assumptions: unbounded engines prove, bounded runs never do. Counterexample means a concrete trace breaks it, named by its earliest failing cycle. Inconclusive means undetermined: time ran out, the bound was reached, or the induction step failed without deciding the property. A bounded pass is not a fourth outcome: it is an inconclusive result that states how far it looked, no violation within N steps, and it is signoff-grade only with a justification.
The runs below use one design and one set of properties, the counter, and change one thing at a time. The first block proves the good design outright. The next three run the counter with the wrap-at-10 bug: depth 10 passes, because the bug first shows at step 10, which a depth-10 run never reaches; depth 11 fails with the trace; depth 20 fails again. Same properties, four answers, and every difference is in the bound or the design variant, never a disagreement about one model.
// formal: prove 4 expect pass slang top mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
// sticky flag: the counter has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmoduleThe good design proves outright: base case and induction step both pass at depth 4. The header says prove, the expectation says pass, and the lesson claims a full proof for this model under its assumptions.
// formal: bmc 10 expect pass slang top mod10_counter define BUG=1
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
// sticky flag: the counter has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmoduleThe buggy design passes at depth 10: no violation within 10 steps. The bug fires at step 10, which this bound does not reach, so the pass is correct and narrow: bounded to 10, nothing more.
// formal: bmc 11 expect fail slang top mod10_counter define BUG=1
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
// sticky flag: the counter has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmoduleOne step deeper, the same model fails: count 9 is reached at step 10 and the terminal pulse is wrongly low there. Read the trace cycle by cycle: reset, then one count per enabled cycle, and the missing pulse at step 10. The depth-10 pass did not contradict this; it never looked that far.
// formal: bmc 20 expect fail slang top mod10_counter define BUG=1
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
// rst (synchronous, active high) : count <= 0
// en = 1 : count <= (count == 9) ? 0 : count + 1
// en = 0 : count holds
// tc = en && (count == 9) : terminal-count pulse (combinational)
// States 10..15 exist in the 4-bit register but are unreachable from reset.
// BUG: 0 none, 1 wraps at 10 instead of 9 (counts 0..10, a mod-11 counter).
// HELPER: 1 (default) includes the helper invariant count <= 9; 0 leaves count != 15 alone.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire en,
output reg [3:0] count,
output wire tc
);
wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
assign tc = en && (count == last);
always @(posedge clk) begin
if (rst) count <= 4'd0;
else if (en) count <= (count == last) ? 4'd0 : count + 4'd1;
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// P2: count is never 15. True on every reachable state, but NOT inductive on its own: the
// unreachable states 10..14 satisfy it and lead to 15 (and en = 0 lets a state repeat forever,
// so no k of k-induction closes it).
always @(*) if (!init) a_not15: assert (count != 4'd15);
// P1 / helper: count <= 9. Inductive on its own (k = 1), and it makes a_not15 inductive.
generate if (HELPER) begin : g_helper
always @(*) if (!init) a_range: assert (count <= 4'd9);
end endgenerate
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
always @(posedge clk) if (!init && !$past(rst)) begin
a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
a_hold: assert ($past(en) || count == $past(count));
end
// sticky flag: the counter has wrapped at least once
reg wrapped;
always @(posedge clk) begin
if (rst) wrapped <= 1'b0;
else if (tc) wrapped <= 1'b1;
end
always @(*) if (!init) begin
c_nine: cover (count == 4'd9);
c_tc: cover (tc);
c_wrap: cover (wrapped && count == 4'd3);
end
`endif
endmoduleDeeper still, the counterexample stays: once a trace exists at some depth, every deeper run on the same model contains it.
Run | Model | Result | What it means |
|---|---|---|---|
prove, depth 4 | Good design | Proven | Base and step both pass: holds for all reachable states |
bmc, depth 10 | Wrap-at-10 bug | Inconclusive, bounded to 10 | No violation within 10 steps; step 10 never examined |
bmc, depth 11 | Wrap-at-10 bug | Counterexample at step 10 | A concrete trace exists on this model |
bmc, depth 20 | Wrap-at-10 bug | Counterexample at step 10 | A deeper run on the same model cannot lose the trace |
If the runs disagree, check | Example | How you see it |
|---|---|---|
Design revision or bug variant | BUG=0 against BUG=1 | Parameter list and source revision in the run header |
Assumption set | One run carries an extra assume | Diff the assumption lists |
Reset and initial state | Free start against one reset step | Does every trace begin at reset? |
Bound | Depth 10 against depth 11 | Same module text, different header |
Property text | A guard edited in one copy | Diff the property files |
Every quoted result names its depth and its design variant alongside the verdict.
A bounded pass is never filed as a proof without a bound justification.
When two runs disagree, the review lists what differed before believing either.
When runs disagree, work the checklist in the table in order. The usual culprit is the bound, as above; the dangerous one is an assumption that one run carries and the other does not, because that changes the model. If everything matches and the runs still disagree, suspect the harness wiring and then report a tool defect with both runs attached.
Whether the setups truly match: assumption set, reset model, design revision and bound. A counterexample on a model always beats a proof claim about a different model, so one of the two runs answers a different question.