A one-hot decoder is specified only for counts 0 to 9. Its proof assumes the count stays in that range; the decade counter proves that it does. The system run passes with no assumption at all. Job of this lesson: state the rule, run the three proofs, and show what a fault in the counter, a fault in the decoder and a missing assumption each look like.
The rule: A is proved under an assumption X about its inputs; B is proved, as an assertion on its outputs, to guarantee X; then A and B together satisfy A's guarantee, provided there is no circular dependence. Here X is count <= 9. The counter already carries X as a helper assertion (a_range); the decoder takes X as an assumption on its input when proved alone, and takes nothing when it sits behind the counter.
Obligation | Run | Result |
|---|---|---|
A under X: decoder, assumption on its input | decoder, | Proven, depth 4 |
B guarantees X: counter, | counter file | Proven, depth 4 |
Top: counter driving decoder, no assumption | system | Proven, depth 4 |
// formal: prove 4 expect pass slang top decode10 define ASSUME=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
endmodule
// decode10: turns a decade count into a one-hot vector. It is only specified for counts 0 to 9 (ASSUME=1 states that
// as an assumption on its input; the top module leaves it out, because the counter has to guarantee it).
// BUG=1: the decode is shifted by one place.
module decode10 #(parameter ASSUME = 0, parameter BUG = 0) (
input wire chk, // the properties are only evaluated while chk is high (after the first reset)
input wire [3:0] cnt,
output wire [9:0] oh
);
assign oh = (BUG == 1) ? (10'd1 << (cnt + 4'd1)) : (10'd1 << cnt);
`ifdef FORMAL
generate if (ASSUME) begin : g_assume
always @(*) assume (cnt <= 4'd9);
end endgenerate
// exactly one bit set, and it is the bit the count names
always @(*) if (chk) begin
a_onehot: assert (oh != 10'd0 && (oh & (oh - 10'd1)) == 10'd0);
a_names: assert (oh[cnt]);
end
`endif
endmodule
// sys10: the decade counter driving the decoder. mod10_counter is the counter of the running examples, with its own proofs.
module sys10 #(parameter CBUG = 0, parameter DBUG = 0) (
input wire clk,
input wire rst,
input wire en
);
wire [3:0] count; wire tc;
mod10_counter #(.BUG(CBUG)) u_cnt (.clk(clk), .rst(rst), .en(en), .count(count), .tc(tc));
reg init0 = 1'b1;
always @(posedge clk) init0 <= 1'b0;
wire [9:0] oh;
decode10 #(.ASSUME(0), .BUG(DBUG)) u_dec (.chk(!init0), .cnt(count), .oh(oh));
endmodule// 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
endmodule// formal: prove 4 expect pass slang top sys10
`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
endmodule
// decode10: turns a decade count into a one-hot vector. It is only specified for counts 0 to 9 (ASSUME=1 states that
// as an assumption on its input; the top module leaves it out, because the counter has to guarantee it).
// BUG=1: the decode is shifted by one place.
module decode10 #(parameter ASSUME = 0, parameter BUG = 0) (
input wire chk, // the properties are only evaluated while chk is high (after the first reset)
input wire [3:0] cnt,
output wire [9:0] oh
);
assign oh = (BUG == 1) ? (10'd1 << (cnt + 4'd1)) : (10'd1 << cnt);
`ifdef FORMAL
generate if (ASSUME) begin : g_assume
always @(*) assume (cnt <= 4'd9);
end endgenerate
// exactly one bit set, and it is the bit the count names
always @(*) if (chk) begin
a_onehot: assert (oh != 10'd0 && (oh & (oh - 10'd1)) == 10'd0);
a_names: assert (oh[cnt]);
end
`endif
endmodule
// sys10: the decade counter driving the decoder. mod10_counter is the counter of the running examples, with its own proofs.
module sys10 #(parameter CBUG = 0, parameter DBUG = 0) (
input wire clk,
input wire rst,
input wire en
);
wire [3:0] count; wire tc;
mod10_counter #(.BUG(CBUG)) u_cnt (.clk(clk), .rst(rst), .en(en), .count(count), .tc(tc));
reg init0 = 1'b1;
always @(posedge clk) init0 <= 1'b0;
wire [9:0] oh;
decode10 #(.ASSUME(0), .BUG(DBUG)) u_dec (.chk(!init0), .cnt(count), .oh(oh));
endmoduleNow a fault in each place. The counter with modulus 11 (BUG=1) fails its own proof at step 10 (depth 10 passes), so B no longer guarantees X. The decoder's own proof is a separate run and is unchanged, because it assumes X. The system fails at step 10. The decoder shifted by one place fails its unit proof at once (step 0), and so does the system one step later. With X removed, the decoder fails at step 0 on a count the counter never gives:
// 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
endmodule// formal: bmc 11 expect fail slang top sys10 define CBUG=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
endmodule
// decode10: turns a decade count into a one-hot vector. It is only specified for counts 0 to 9 (ASSUME=1 states that
// as an assumption on its input; the top module leaves it out, because the counter has to guarantee it).
// BUG=1: the decode is shifted by one place.
module decode10 #(parameter ASSUME = 0, parameter BUG = 0) (
input wire chk, // the properties are only evaluated while chk is high (after the first reset)
input wire [3:0] cnt,
output wire [9:0] oh
);
assign oh = (BUG == 1) ? (10'd1 << (cnt + 4'd1)) : (10'd1 << cnt);
`ifdef FORMAL
generate if (ASSUME) begin : g_assume
always @(*) assume (cnt <= 4'd9);
end endgenerate
// exactly one bit set, and it is the bit the count names
always @(*) if (chk) begin
a_onehot: assert (oh != 10'd0 && (oh & (oh - 10'd1)) == 10'd0);
a_names: assert (oh[cnt]);
end
`endif
endmodule
// sys10: the decade counter driving the decoder. mod10_counter is the counter of the running examples, with its own proofs.
module sys10 #(parameter CBUG = 0, parameter DBUG = 0) (
input wire clk,
input wire rst,
input wire en
);
wire [3:0] count; wire tc;
mod10_counter #(.BUG(CBUG)) u_cnt (.clk(clk), .rst(rst), .en(en), .count(count), .tc(tc));
reg init0 = 1'b1;
always @(posedge clk) init0 <= 1'b0;
wire [9:0] oh;
decode10 #(.ASSUME(0), .BUG(DBUG)) u_dec (.chk(!init0), .cnt(count), .oh(oh));
endmodule// formal: bmc 2 expect fail slang top sys10 define DBUG=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
endmodule
// decode10: turns a decade count into a one-hot vector. It is only specified for counts 0 to 9 (ASSUME=1 states that
// as an assumption on its input; the top module leaves it out, because the counter has to guarantee it).
// BUG=1: the decode is shifted by one place.
module decode10 #(parameter ASSUME = 0, parameter BUG = 0) (
input wire chk, // the properties are only evaluated while chk is high (after the first reset)
input wire [3:0] cnt,
output wire [9:0] oh
);
assign oh = (BUG == 1) ? (10'd1 << (cnt + 4'd1)) : (10'd1 << cnt);
`ifdef FORMAL
generate if (ASSUME) begin : g_assume
always @(*) assume (cnt <= 4'd9);
end endgenerate
// exactly one bit set, and it is the bit the count names
always @(*) if (chk) begin
a_onehot: assert (oh != 10'd0 && (oh & (oh - 10'd1)) == 10'd0);
a_names: assert (oh[cnt]);
end
`endif
endmodule
// sys10: the decade counter driving the decoder. mod10_counter is the counter of the running examples, with its own proofs.
module sys10 #(parameter CBUG = 0, parameter DBUG = 0) (
input wire clk,
input wire rst,
input wire en
);
wire [3:0] count; wire tc;
mod10_counter #(.BUG(CBUG)) u_cnt (.clk(clk), .rst(rst), .en(en), .count(count), .tc(tc));
reg init0 = 1'b1;
always @(posedge clk) init0 <= 1'b0;
wire [9:0] oh;
decode10 #(.ASSUME(0), .BUG(DBUG)) u_dec (.chk(!init0), .cnt(count), .oh(oh));
endmodule// formal: bmc 1 expect fail slang top decode10 define ASSUME=1 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
endmodule
// decode10: turns a decade count into a one-hot vector. It is only specified for counts 0 to 9 (ASSUME=1 states that
// as an assumption on its input; the top module leaves it out, because the counter has to guarantee it).
// BUG=1: the decode is shifted by one place.
module decode10 #(parameter ASSUME = 0, parameter BUG = 0) (
input wire chk, // the properties are only evaluated while chk is high (after the first reset)
input wire [3:0] cnt,
output wire [9:0] oh
);
assign oh = (BUG == 1) ? (10'd1 << (cnt + 4'd1)) : (10'd1 << cnt);
`ifdef FORMAL
generate if (ASSUME) begin : g_assume
always @(*) assume (cnt <= 4'd9);
end endgenerate
// exactly one bit set, and it is the bit the count names
always @(*) if (chk) begin
a_onehot: assert (oh != 10'd0 && (oh & (oh - 10'd1)) == 10'd0);
a_names: assert (oh[cnt]);
end
`endif
endmodule
// sys10: the decade counter driving the decoder. mod10_counter is the counter of the running examples, with its own proofs.
module sys10 #(parameter CBUG = 0, parameter DBUG = 0) (
input wire clk,
input wire rst,
input wire en
);
wire [3:0] count; wire tc;
mod10_counter #(.BUG(CBUG)) u_cnt (.clk(clk), .rst(rst), .en(en), .count(count), .tc(tc));
reg init0 = 1'b1;
always @(posedge clk) init0 <= 1'b0;
wire [9:0] oh;
decode10 #(.ASSUME(0), .BUG(DBUG)) u_dec (.chk(!init0), .cnt(count), .oh(oh));
endmodule// formal: bmc 1 expect fail slang top decode10 define ASSUME=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
endmodule
// decode10: turns a decade count into a one-hot vector. It is only specified for counts 0 to 9 (ASSUME=1 states that
// as an assumption on its input; the top module leaves it out, because the counter has to guarantee it).
// BUG=1: the decode is shifted by one place.
module decode10 #(parameter ASSUME = 0, parameter BUG = 0) (
input wire chk, // the properties are only evaluated while chk is high (after the first reset)
input wire [3:0] cnt,
output wire [9:0] oh
);
assign oh = (BUG == 1) ? (10'd1 << (cnt + 4'd1)) : (10'd1 << cnt);
`ifdef FORMAL
generate if (ASSUME) begin : g_assume
always @(*) assume (cnt <= 4'd9);
end endgenerate
// exactly one bit set, and it is the bit the count names
always @(*) if (chk) begin
a_onehot: assert (oh != 10'd0 && (oh & (oh - 10'd1)) == 10'd0);
a_names: assert (oh[cnt]);
end
`endif
endmodule
// sys10: the decade counter driving the decoder. mod10_counter is the counter of the running examples, with its own proofs.
module sys10 #(parameter CBUG = 0, parameter DBUG = 0) (
input wire clk,
input wire rst,
input wire en
);
wire [3:0] count; wire tc;
mod10_counter #(.BUG(CBUG)) u_cnt (.clk(clk), .rst(rst), .en(en), .count(count), .tc(tc));
reg init0 = 1'b1;
always @(posedge clk) init0 <= 1'b0;
wire [9:0] oh;
decode10 #(.ASSUME(0), .BUG(DBUG)) u_dec (.chk(!init0), .cnt(count), .oh(oh));
endmoduleFault | A under X | B guarantees X | Top |
|---|---|---|---|
Counter counts to 10 | Proven (assumes X) | Fails, step 10 | Fails, step 10 |
Decoder shifted by one | Fails, step 0 | Proven | Fails, step 1 |
X left out | Fails, step 0, on counts 10 to 15 | Proven | Proven |
The first row is why the proof of A alone is never enough: it passes with a faulty neighbour. The last row is why the rule needs X: without it A fails on inputs nobody can produce, a false counterexample.
A table row for X: where it is assumed, where it is proved, and the run that proves it.
The proof of B asserts X on B's outputs, as an assertion that is itself proved, not assumed.
A fault planted in B fails B's proof while A's unit proof still passes. If it does not, the proof of B is missing a property.
When the top fails and both unit proofs pass, the assumption of A and the assertion of B are not the same statement: compare their text. When A fails alone on a trace no neighbour can produce, a rule is missing from A's assumptions.
The counter's own proof of B. The decoder's unit proof still passes, because it assumes X, and the top proof only says something is wrong.