Bounded model checking and induction

Bounded model checking (BMC)

BMC unrolls the design k times: copy the transition logic once per cycle, connect the next-state outputs of copy i to the current-state inputs of copy i+1, constrain copy 0 to the initial state, and ask the SAT solver whether the property can fail in any of the k frames.

If the solver finds an assignment, it is a counterexample of length ≤ k. If not, the property holds for the first k cycles — a bounded proof. BMC is excellent at finding bugs quickly, but on its own it can never prove a property for all time.

Induction: proving for all time

Mathematical induction gives an unbounded proof in two steps:

• Base case — P holds in the initial states (and, for k-induction, in the first k cycles: that is BMC).
• Inductive step — from any state where P has held for k consecutive cycles, P still holds in the next cycle.

The catch is the word any: the step starts from arbitrary states, including unreachable ones.

When induction fails on a true property

// decade_counter.sv — counts 0..9 and wraps
module decade_counter (
  input  logic       clk, rst, en,
  output logic [3:0] cnt
);
  always_ff @(posedge clk) begin
    if (rst)           cnt <= 4'd0;
    else if (en)       cnt <= (cnt == 4'd9) ? 4'd0 : cnt + 4'd1;
  end
endmodule

// decade_counter_fv.sv
module decade_counter_fv (input logic clk, rst, en);
  logic [3:0] cnt;
  decade_counter dut (.*);

  initial assume (rst);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  // True, but NOT inductive on its own:
  a_never_12: assert property (cnt != 4'd12);

  // Helper invariant: inductive, and it implies a_never_12
  a_range:    assert property (cnt <= 4'd9);
endmodule

Try to prove a_never_12 by 1-induction alone. The inductive step may pick the unreachable state cnt = 11: it satisfies the property (11 ≠ 12), but one increment later cnt = 12. The step fails, even though the property is true in every reachable state. This is called an induction counterexample — the trace does not start from reset.

The fix is to strengthen the induction with a helper assertion that rules out the unreachable states. a_range (cnt ≤ 9) is itself inductive: from any state with cnt ≤ 9, the next value is also ≤ 9. Once proven, tools use it as a lemma, and a_never_12 follows immediately.

PDR / IC3: induction that finds its own helpers

Property-directed reachability (PDR, also called IC3) is a SAT-based algorithm that automates this strengthening: it incrementally learns small clauses (like "cnt is not 11") that block unreachable predecessors of bad states, until the learned clauses form an inductive invariant. PDR is one of the most successful unbounded engines in both commercial and open-source tools. Even so, a well-chosen human helper assertion often turns an hours-long PDR run into seconds.

Chapter takeaways