Depth is the most argued-about number in formal reviews, and most arguments come from treating it as a dial rather than a structure. A bounded check to depth N literally builds N copies of the design logic, one per cycle, wired register to register from the reset state, and asks the solver whether any copy can break an assertion while every assumption holds. Once you see the copies, depth choice, cost growth and the meaning of a pass all become mechanical.
Unrolling turns time into space. Copy 0 holds the power-up state, with reset forced high; copy 1 holds the state after the reset edge, with its registers fed by copy 0; copy 2 is fed by copy 1, and so on. The solver picks the inputs in every copy at once: the question is whether any assignment across all the copies falsifies an assertion in any copy. A counterexample is the solver's answer written back as a trace. It is a shortest one in practice because the runs are made at depth 1, 2, 3 and so on in turn, or the solver minimises: a single query at a large depth is free to return a longer trace.
The cost follows the same picture. With G gates and F state bits over N cycles, the formula needs about 3 clauses per gate per cycle plus F register-link equalities per cycle. For the illustrative sizes below, 50,000 gates and 2,000 state bits, that is 152,000 clauses per step and 4.56 million at depth 30: routine for a modern solver, growing linearly with depth until memory says otherwise (where that happens depends on the tool and the machine). A word-level solver keeps the same copies but states wider constraints instead of clauses.
Read it left to right: start in reset, obey the transition relation at every step, and break the property in at least one copy. Satisfiable means a counterexample exists within N steps; unsatisfiable means bounded to N. One convention: the formula has N + 1 states, s_0 to s_N, while a run configured with depth D examines steps 0 to D minus 1, so D = N + 1.
The FIFO variant that accepts a pop while empty is unrolled by hand to three copies below: copy 1 is the first state after reset with count 0, the solver sets pop high, and copy 2 holds count 7 because 0 minus 1 wraps in three bits. The occupancy property count within 4 fails in copy 2, so the run at depth 3 finds it and the run at depth 2 cannot. The decade counter makes the opposite point: its wrap needs ten enabled cycles, so three copies cannot see it.
# not-run: illustrative trace, not executable here
copy 0 (step 0): rst = 1 (assumed), every register arbitrary
copy 1 (step 1): count = 0 after the reset edge; the solver sets pop = 1
copy 2 (step 2): the faulty FIFO accepts the pop while empty: count = 0 - 1 = 7 (3 bits)
question: is count <= 4 false in any copy? copy 2: yes (7 > 4) -> counterexample, depth 3
decade counter, three copies: count is 0, then at most 1, then at most 2: no copy can hold 9 or 10// formal: bmc 20 expect pass slang top sync_fifo
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
// This copy keeps the control properties only: no data-integrity harness.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
`endif
endmoduleThe good FIFO passes: no input sequence of up to 20 steps breaks occupancy, flags, pointer consistency or the transition rules. The verdict is bounded to 20, not proven.
// formal: bmc 2 expect pass slang top sync_fifo define BUG=2
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
// This copy keeps the control properties only: no data-integrity harness.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
`endif
endmoduleTwo copies are not enough for the pop-while-empty variant: the faulty pop is issued in copy 1 and its effect appears in copy 2, which depth 2 does not include. Bounded to 2.
// formal: bmc 3 expect fail slang top sync_fifo define BUG=2
`define FORMAL
// sync_fifo: 4-entry, 8-bit synchronous FIFO. Running example of the Formal course.
// Synchronous active-high reset. count is an output so properties can see it.
// BUG selects a planted bug: 0 none, 1 push accepted when full, 2 pop accepted when
// empty, 3 full flag one entry early, 4 simultaneous push+pop miscounts, 5 write
// data bit 7 stuck at 0.
// This copy keeps the control properties only: no data-integrity harness.
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; // forgets the pop
else count <= count + {2'b0, do_push} - {2'b0, do_pop};
end
end
`ifdef FORMAL
// ---- harness: first cycle is reset, state before it is arbitrary ----
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// ---- safety properties (after the reset cycle) ----
always @(*) if (!init) begin
a_range: assert (count <= 3'd4); // no overflow, no underflow wrap
a_flags: assert (full == (count == 3'd4) && empty == (count == 3'd0));
a_not_both: assert (!(full && empty));
// occupancy equals pointer distance (mod 4)
a_ptr: assert (count[1:0] == (wptr - rptr));
end
// ---- transition properties (use history: skip the cycle after reset) ----
always @(posedge clk) if (!init && !$past(rst)) begin
// push alone when not full adds one; pop alone when not empty removes one
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);
// push into a full FIFO (and no pop) is ignored: occupancy unchanged
a_ovf_ign: assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
// simultaneous push and pop (neither empty nor full) leaves occupancy unchanged
a_both: assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
end
`endif
endmoduleThree copies find it, exactly as in the hand unrolling: reset, one pop, count reads 7 at step 2.
def clauses(gates, flops, depth, link_flops=True, links_per_step=True):
links = flops if link_flops else 0
if links_per_step:
return (3 * gates + links) * depth
return 3 * gates * depth + links # links counted once: wrong
def check(model):
assert model(50000, 2000, 1) == 152000 # one step
assert model(50000, 2000, 30) == 4560000 # depth 30
assert model(50000, 2000, 60) == 2 * model(50000, 2000, 30) # growth is linear in depth
check(clauses)
# injected model 1: forgets the register-link equalities
# injected model 2: counts the links once instead of once per step
broken = [lambda g, f, d: clauses(g, f, d, link_flops=False),
lambda g, f, d: clauses(g, f, d, links_per_step=False)]
for model in broken:
caught = False
try:
check(model)
except AssertionError:
caught = True
assert caught, "the clause check accepted a wrong model"
print("PASS: 152000 clauses per step, 4.56 million at depth 30, linear growth; two miscounts caught")The depth is justified against the states the property needs, never a round number inherited from another block.
Cost talk quotes gates times depth, and deep runs carry a memory ceiling, not just a time budget.
A bounded pass is filed with its depth in the same sentence as the verdict.
Recheck any bounded pass by asking what the deepest interesting state needs: if the property cares about a full FIFO, confirm the bound reaches at least one reset plus four pushes plus the check cycle. If the run is slow, confirm the cone bit count before lengthening the timeout: a 32-bit datapath in the cone dwarfs any depth effect.
Because the runs are made at depth 1, 2, 3 in turn, or the solver is asked to minimise, so the first depth that is satisfiable is the shallowest violation. A single query at a large depth is allowed to return a longer trace. Either way the trace is an excellent bug report and says nothing about completeness.