Every panel asks some version of these six first. Each answer has the four parts, the run it rests on, the trap and the lesson that teaches it, and takes about three minutes aloud.
Assumption: reset model, free inputs and assumption list stated. Mechanism: speed fits a small cone, such as the 4-entry FIFO control set closing at k of 2, but it is also the signature of vacuity, a disconnected property or a reset held forever. Trade-off: a deeper rerun settles nothing on an empty harness; the five acceptance checks do. Evidence: antecedent cover reached at a step, activity cover, cone contents, a failing mutant per property class, every assume owned. Trap: answering yes or no. See antecedent covers.
Assumption: the interface specification says which side owes each rule. Mechanism: assume on inputs what the neighbour owes you, assert on outputs what you owe, cover that both sides can act. Trade-off: asserting on both sides gives false counterexamples from illegal inputs; assuming everything passes vacuously. Evidence: each assume mapped to the neighbour assertion that proves it, and a run with one assume removed showing the false counterexample it held back. Trap: polarity. See assume versus assert by side.
Assumption: fixed reset sequence, free inputs, depth stated. Mechanism: unroll the transition relation N times and ask the solver for a violation; a pass is bounded to N, signoff-grade only with a reason: depth at least reset plus trigger length plus worst-case latency plus 1, a diameter, or an inductive proof. Trade-off: depth buys bug-finding, not proof. Evidence: the pair below. Trap: calling the depth-10 pass a proof. See choosing a depth.
// 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.
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);
always @(*) if (!init) a_not15: assert (count != 4'd15);
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
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 mod10_counter define BUG=1
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
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);
always @(*) if (!init) a_not15: assert (count != 4'd15);
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
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
endmoduleRead it: count 0 at step 1, one more per enabled cycle, 9 with enable high at step 10, where the terminal pulse is expected but the wrap constant 10 keeps counting. Root cause: modulus 11. Fix: wrap at 9.
Assumption: same reset model. Mechanism: the base case checks the first k states from reset; the step assumes any k consecutive states satisfy the property and checks the next, from arbitrary states, reachable or not. 'Count never 15' is true but not inductive: the unreachable chain 10 to 14 satisfies it and leads to 15. The helper 'count at most 9' closes it at k of 1, the whole set at 2. Trade-off: raising k never closes it; one invariant does. Evidence: the unproven run beside the proven one, differing only by the helper. Trap: reading a failing step as an RTL bug. See CTIs and unreachable states.
// 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.
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);
always @(*) if (!init) a_not15: assert (count != 4'd15);
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
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 mod10_counter
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
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);
always @(*) if (!init) a_not15: assert (count != 4'd15);
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
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
endmoduleAssumption: reset once; push and pop are free, including a push when full, because that is the case the property guards; no assumption on data. Mechanism: the invariant 'count at most DEPTH' uses the depth only as a parameter and is inductive, so the same proof runs at any DEPTH, 5 (not a power of two) and 12 included. A tool proves one instance per run: 'for any depth' is sampled instances plus the argument that the step never uses the size. The overflow bug needs entries plus 3 as depth: 7 on the 4-entry FIFO, 8 at DEPTH 5, 15 at DEPTH 12. Trade-off: one size is read directly; the invariant covers every size, for data-independent properties. Evidence: the runs below. Trap: a depth one short passes. See FIFO ordering and data integrity.
// formal: prove 4 expect pass slang top occ define DEPTH=5
`define FORMAL
// Lesson-local demo: occupancy counter of a FIFO with a parameterised depth; BUG=1 accepts a push when full.
module occ #(parameter DEPTH = 4, parameter BUG = 0) (
input wire clk, input wire rst, input wire push, input wire pop,
output wire full, output wire empty, output reg [4:0] count
);
assign full = (count == DEPTH);
assign empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) count <= 5'd0;
else count <= count + {4'b0, do_push} - {4'b0, do_pop};
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= DEPTH);
`endif
endmodule// formal: prove 4 expect pass slang top occ define DEPTH=12
`define FORMAL
// Lesson-local demo: occupancy counter of a FIFO with a parameterised depth; BUG=1 accepts a push when full.
module occ #(parameter DEPTH = 4, parameter BUG = 0) (
input wire clk, input wire rst, input wire push, input wire pop,
output wire full, output wire empty, output reg [4:0] count
);
assign full = (count == DEPTH);
assign empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) count <= 5'd0;
else count <= count + {4'b0, do_push} - {4'b0, do_pop};
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= DEPTH);
`endif
endmodule// formal: bmc 7 expect pass slang top occ define DEPTH=5 define BUG=1
`define FORMAL
// Lesson-local demo: occupancy counter of a FIFO with a parameterised depth; BUG=1 accepts a push when full.
module occ #(parameter DEPTH = 4, parameter BUG = 0) (
input wire clk, input wire rst, input wire push, input wire pop,
output wire full, output wire empty, output reg [4:0] count
);
assign full = (count == DEPTH);
assign empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) count <= 5'd0;
else count <= count + {4'b0, do_push} - {4'b0, do_pop};
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= DEPTH);
`endif
endmodule// formal: bmc 8 expect fail slang top occ define DEPTH=5 define BUG=1
`define FORMAL
// Lesson-local demo: occupancy counter of a FIFO with a parameterised depth; BUG=1 accepts a push when full.
module occ #(parameter DEPTH = 4, parameter BUG = 0) (
input wire clk, input wire rst, input wire push, input wire pop,
output wire full, output wire empty, output reg [4:0] count
);
assign full = (count == DEPTH);
assign empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) count <= 5'd0;
else count <= count + {4'b0, do_push} - {4'b0, do_pop};
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= DEPTH);
`endif
endmodule// formal: bmc 14 expect pass slang top occ define DEPTH=12 define BUG=1
`define FORMAL
// Lesson-local demo: occupancy counter of a FIFO with a parameterised depth; BUG=1 accepts a push when full.
module occ #(parameter DEPTH = 4, parameter BUG = 0) (
input wire clk, input wire rst, input wire push, input wire pop,
output wire full, output wire empty, output reg [4:0] count
);
assign full = (count == DEPTH);
assign empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) count <= 5'd0;
else count <= count + {4'b0, do_push} - {4'b0, do_pop};
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= DEPTH);
`endif
endmodule// formal: bmc 15 expect fail slang top occ define DEPTH=12 define BUG=1
`define FORMAL
// Lesson-local demo: occupancy counter of a FIFO with a parameterised depth; BUG=1 accepts a push when full.
module occ #(parameter DEPTH = 4, parameter BUG = 0) (
input wire clk, input wire rst, input wire push, input wire pop,
output wire full, output wire empty, output reg [4:0] count
);
assign full = (count == DEPTH);
assign empty = (count == 0);
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && !empty;
always @(posedge clk) begin
if (rst) count <= 5'd0;
else count <= count + {4'b0, do_push} - {4'b0, do_pop};
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) a_range: assert (count <= DEPTH);
`endif
endmodule// formal: bmc 6 expect pass slang top sync_fifo define BUG=1
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule// formal: bmc 7 expect fail slang top sync_fifo define BUG=1
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
input wire clk,
input wire rst,
input wire push,
input wire [7:0] wdata,
input wire pop,
output wire [7:0] rdata,
output wire full,
output wire empty,
output reg [2:0] count
);
reg [7:0] mem [0:3];
reg [1:0] wptr, rptr;
assign full = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
assign empty = (count == 3'd0);
assign rdata = mem[rptr];
wire do_push = push && (!full || BUG == 1);
wire do_pop = pop && (!empty || BUG == 2);
always @(posedge clk) begin
if (rst) begin
wptr <= 2'd0;
rptr <= 2'd0;
count <= 3'd0;
end else begin
if (do_push) begin
mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
wptr <= wptr + 2'd1;
end
if (do_pop) rptr <= rptr + 2'd1;
if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
always @(*) if (!init) begin
a_range: assert (count <= 3'd4);
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
a_ptr: assert (count[1:0] == (wptr - rptr));
end
always @(posedge clk) if (!init && !$past(rst)) begin
a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
a_pop_dec: assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
(* anyconst *) wire [1:0] tslot;
reg [1:0] tslot_q;
always @(posedge clk) tslot_q <= tslot;
always @(*) if (!init) assume (tslot == tslot_q);
reg tv;
reg [7:0] td;
always @(posedge clk) begin
if (rst) tv <= 1'b0;
else begin
if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
else if (do_pop && rptr == tslot) tv <= 1'b0;
end
end
always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
generate if (HELPER) begin : g_helper
always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
end endgenerate
always @(*) if (!init) begin
c_full: cover (count == 3'd4);
c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
end
always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmoduleAssumption: none on the requesters for the bounded form, because the 4-way round robin grants whenever any request exists; the unbounded 'eventually' would need fairness on the environment. Mechanism: no liveness engine runs, so write bounded response, a safety property: a continuously requesting requester waits at most 3 cycles and is granted in the fourth. Trade-off: the bounded form proves with a stated window; the unbounded form needs fairness and a lasso engine. Evidence: the wait bound proved, the contention cover reached at step 4, the starvation mutant failing at depth 6 with the helper assertions off (depth 5 passes; with them on it fails at depth 3), all run in the deadlock scenario. Trap: fairness on the grant output, which assumes the answer. See bounded response is safety.
A finite prefix that waits too long already violates it. Eventually needs an infinite loop, a lasso, to fail, which a bounded run cannot produce.