A property passed on a design with an obvious bug: the terminal pulse fired a cycle late and nobody noticed, because the assertion checked a condition that could never fail. The proof faithfully proved the wrong thing. Safety properties look simple, which is why their bound and their reference deserve a lesson of their own.
Job of this lesson: define a safety property as an invariant, show its counterexample as a finite path, and demonstrate the two classic ways to write one that cannot fail.
A safety property says the bad thing never happens: the count never exceeds 9, the occupancy never exceeds 4. As an invariant it must hold in every reachable state, and its counterexample is a finite path from reset to a violation. That suits a bounded check: unroll N steps and ask the solver for a path to the bad state.
Two writing mistakes survive every run. A bound that is too weak passes on a broken design because it allows the bad value. A self-referential check compares a signal with a copy of the same logic and cannot fail. The defence is to mutate the design (plant a bug and see the property fail) and to cover the bad value.
The good design proves: the count never exceeds 9, the pulse matches the count, and the step and hold rules all hold.
// 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
endmoduleThe pulse property alone, written from the specification (the pulse is high when enabled at count 9), catches the bug that wraps at 10. The buggy counter moves on to 10 instead of raising the pulse at 9, so the check fails at step 10:
// 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);
// from the specification: the pulse is high when enabled at count 9
always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
`endif
endmoduleStep | en | count | tc | Note |
|---|---|---|---|---|
0 | - | arbitrary | - | Power-up; reset asserted. |
1 to 9 | 1 | 0 to 8 | 0 | Counting up. |
10 | 1 | 9 | 0 | The specification expects tc = 1 here: a_tc fails. |
11 | 1 | 10 | 0 | The bug lets the count reach 10. |
Now the two mistakes. A weak bound, count <= 10, is true of the buggy counter, so the proof of the wrong thing is complete:
// formal: prove 4 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);
// wrong bound: 10 is allowed, so the bug is invisible
always @(*) if (!init) a_weak: assert (count <= 4'd10);
always @(*) if (!init) c_ten: cover (count == 4'd10);
`endif
endmoduleThe cover of the value that the bound allows is the exposure: the same file, with only its header changed, reaches count 10 on the buggy counter at depth 12. (The bound allows 10, so it does not block the trace.)
// formal: cover 12 expect reached 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);
// same file as the proof above: only the header changed
always @(*) if (!init) a_weak: assert (count <= 4'd10);
always @(*) if (!init) c_ten: cover (count == 4'd10);
`endif
endmoduleThe self-referential check compares the pulse with the expression that builds it, so it proves on the buggy counter too:
// formal: prove 4 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);
// repeats the implementation (last is 10 in the buggy counter), not the specification (9)
always @(*) if (!init) a_self: assert (tc == (en && count == last));
`endif
endmoduleBoth passes are partnered by the specification property above, which fails on the same mutant. A property that survives its own mutant is a rumour.
Every safety property is an invariant with its bad state named, and quotes the specification, not the RTL expression.
A cover of the bad value exists and its result is read together with the proof about it.
A mutation of the design flips each property from pass to fail at a stated step.
Read the counterexample as a path: initial state, inputs per cycle, earliest failing step. Check polarity by negating the property in words and confirming the negation is the bad scenario you fear. If a property passes suspiciously fast on a new design, plant a bug first and believe it later.
A cover of count 10 in a file with the weak bound: reached on the buggy counter, so the bound never excluded the bad value. On the good counter a cover that is not reached is inconclusive by itself; the proof of count at most 9 makes it a statement about every depth.
A copy of the implementation fails exactly when the implementation fails to match itself, which is never. Only an independent statement can disagree with the design.