A signoff sheet said the decade counter was proven, yet in the lab its terminal pulse arrived one count late. The sheet had recorded a bounded check at depth 10 as a proof; the bug needs depth 11. The tool was fine; the reader misread the result. This lesson fixes the vocabulary so that cannot happen.
Job of this lesson: define proven, counterexample and inconclusive once, with what each demands next, and show four statuses on one design.
A formal run checks a property against the model: the design plus the harness (the reset sequence, the free inputs, every assumption). The answer is relative to that model and is one of three outcomes.
Outcome | Meaning | What it demands next |
|---|---|---|
Proven | Holds for every behaviour of the stated model and assumptions. | Keep the assumption list; rerun on every RTL change. |
Counterexample | A concrete trace that breaks the property, ending at a stated step. | Triage: design bug, missing assumption or model artefact. |
Inconclusive | Undetermined: bound reached, time-out, or the induction step (a check from any state) failed. | Justify the bound, extend the run or strengthen the proof. |
A bounded pass, “no counterexample up to depth N”, written “bounded to N”, is a sound and stated result that proves nothing unbounded, so it is reported under the third row. A counterexample always wins: if a bounded check finds one, no run on the same model, assumptions and reset can report a proof.
Each block starts with a proof header (How to Use This Course explains the words): prove N is a bounded check to depth N plus an induction step (a check that starts from any state, not only from reset); bmc N is the bounded check alone; cover N searches for a witness; expect is the outcome the runner must see. define FORMAL switches on the property part of the file.
The running design is a 4-bit decade counter that counts 0 to 9 and wraps, with a terminal pulse at 9: 10 of its 16 states are reachable, 6 (10 to 15) are not. Run A is a full proof of the good design: the base case and the induction step both pass (the set needs induction depth 2).
// 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, 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
endmoduleRun B plants a bug, a deliberate defect that shows the proof can fail: the wrap constant is 10, not 9.
// 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, 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
endmoduleStep 0 is the power-up state with reset asserted, step 1 the first state after reset. A check on the current state reports the step where the bad state exists; a check that looks back with $past reports one step later. So the pulse check fails at step 10, the range check at step 11 and the step check at step 12.
Step | en | count | tc (spec says) | Note |
|---|---|---|---|---|
0 | - | arbitrary | - | Power-up; reset asserted. A dash means the input is free. |
1 | 1 | 0 | 0 | First state after reset. |
2 to 9 | 1 | 1 to 8 | 0 | Counting up, one per cycle. |
10 | 1 | 9 | 1 | The design shows 0: a_tc fails here. |
11 | 1 | 10 | 0 | Count outside 0 to 9: a_range fails. |
Run C is the same buggy design one step shorter and it passes: a counterexample at step K needs depth K + 1.
// 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, 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
endmoduleRun D removes the helper invariant count <= 9 (an extra true statement that gives the induction step something to stand on). The bounded check passes but the induction step fails: inconclusive.
// formal: prove 10 expect unproven slang top mod10_counter define HELPER=0
`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, 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 step starts from any state, including the unreachable values 10 to 14, which satisfy “count is never 15” and lead to 15. That trace is spurious; the design is fine and the proof is unfinished. Run A, with the helper restored, is its partner.
Every result names the model, the assumption list, and the depth or proof form.
A bounded pass is written “bounded to N”; time-outs are counted apart from passes.
Read the status per property, not the summary line: one failing property among twenty passing ones is still a counterexample. When a run ends without a proof, record which part gave up: the bound, the clock, or the induction step.
Only the depth changed: 10 versus 11. Claim “bounded to 10”, never “proven”.
The induction step fails from unreachable states, so there is no unbounded argument.