k-Induction

Prove a property for all time with a base case and an induction step, and read an induction failure as a missing invariant, not a bug.

Lesson: F2.4
Time: 20 min
Runs on: SymbiYosys
Check: 4 questions

A FIFO property returned UNKNOWN in prove mode. The induction trace began with a count and pointers that no sequence of writes and reads can produce. The engineer debugged the RTL for an hour before noticing the base case had passed.

Two Runs, One Proof

Two Runs Make One ProofThe base case is a BMC from reset. The step drops reset and asks whether k good states can be followed by a bad one.

Read the diagram as text

Base case: copy 0 held to reset
k copies from reset: property checked in every copy
basecase PASS: BMC to depth k finds nothing
Induction step: copy 0 is any state
k copies assumed good: the property holds in each
copy k+1: property must hold here too

Base case → k copies from reset
k copies from reset → basecase PASS
Induction step → k copies assumed good
k copies assumed good → copy k+1: one more step

Both pass: the property holds in every reachable state. Base passes and step fails: UNKNOWN.

k-induction proves a safety property in two halves. The base case is BMC of depth k from reset. The step takes any k consecutive states where the property holds, with no reset, and shows the next state is good too. SBY runs them as basecase and induction.

Measured summary of fifo16 at depth 12: the base case passed, the step failed.

summary: engine_0 (smtbmc yices) returned pass for basecase
summary: engine_0 (smtbmc yices) returned FAIL for induction
summary: counterexample trace [induction]: job/engine_0/trace_induct.vcd
summary:   failed assertion top._witness_.assert_top_sv_20_assert_30 at top.sv:20.16-20.40
DONE (UNKNOWN, rc=4)

The Step Starts Anywhere

The induction step starts anywhere

No reset in this run. The solver picks the first state, keeps the property true for 11 samples, then breaks it.

wr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15
Assumed true (not empty)
Assumed for induction
wr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15
Assumed true (not empty)
Assumed for induction
wr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15
Assumed true (not empty)
Assumed for induction
wr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15
Assumed true (not empty)
Assumed for induction
wr=0, rd=1, rst=0
count=1, wr_ptr=0, rd_ptr=15
Assumed true (not empty)
Assumed for induction
wr=0, rd=0, rst=0
count=0, wr_ptr=0, rd_ptr=16
empty, pointers differ
× Fails
wr=0, rd=0, rst=0
count=0, wr_ptr=0, rd_ptr=16
SBY reports the failure
× Fails

Select a frame to inspect its inputs and assertion.

Measured trace_induct.vcd, frames 0, 1, 2, 9, 10, 11, 12 of 13. The FIFO idles until step 10, then one read empties it with the pointers apart.

Because the step starts from any state, it can start in a state reset never reaches. If that state satisfies the property but can reach a bad state, the step fails there. The trace is a counterexample to induction, not a bug.

A good state that is never reached

Reachable states keep count equal to wr_ptr - rd_ptr. The induction start breaks that relation, and one read from it is bad.

Measured start: count = 1, wr_ptr = 0, rd_ptr = 15, so wr_ptr − rd_ptr = 17 (mod 32). The helper count == wr_ptr - rd_ptr is false there, so it cuts this state off.

Read the states and transitions

c=0: initial, depth 0.
c=1: reachable, depth 1.
c=2: reachable, depth 2.
c=1: unreachable, depth 0.
bad: bad, depth 1.
c=0 → c=1.
c=1 → c=0.
c=1 → c=2.
c=2 → c=1.
c=1 → bad (induction candidate).

Illustration. Reachable count values drawn for 0 to 2 only. The unreachable state is the measured induction start.

Add the Invariant

The rule in concurrent SVA

assert property (@(posedge clk) disable iff (rst)
  empty |-> wr_ptr == rd_ptr);

Not inductive alone: UNKNOWN at depth 12.

Two helper assertions

assert(count == wr_ptr - rd_ptr);   // helper 1
assert(count <= 5'd16);             // helper 2

Asserted, so they are proven too.

Task	Depth	Measured result	Time
no helpers	12	UNKNOWN	0.6 s
helpers	1	UNKNOWN	0.5 s
helpers	2	PASS	0.5 s
no helpers, deeper	16	UNKNOWN	0.9 s
no helpers, deeper	24	UNKNOWN	5.8 s

All with smtbmc yices in prove mode. The one thing changed is the two helper lines, or the depth.

A helper invariant is a fact about internal state that is itself inductive and rules out the strange start states. It must be asserted. An assumed helper would hide every state that breaks it, including real bugs (F3.2).

Why depth 2 and not 1? A clocked check at step t reads the state sampled at t − 1, so a depth-1 window assumes nothing about any state. Depth 2 assumes one good state and checks the next: the classic one-step induction. The ab_cnt helper below behaves the same way.

Depth Alone Can Stay UNKNOWN

Measured induction trace (trace_induct.vcd). Step 0 is chosen by the solver, not by reset.

In the measured trace the FIFO idles in the strange state for 10 steps before it reads. Nothing in a plain window forbids that, so every longer window can start there too. Depth 24 is still UNKNOWN.

Sheeran, Singh and Stålmarck add a constraint that the k states in the window all differ. With it, k-induction is complete for finite systems, but k may have to be as long as the longest loop-free path. Helpers are the engineer’s tool (F4.6); F2.5 shows an engine that finds them itself.

A Smaller One: ab_cnt

Task	Depth	Measured result	Induction start
`a != 10 \|\| b == 10`	2	UNKNOWN	a = 9, b = 15
same	20	UNKNOWN	not shown
plus `assert(a == b)`	1	UNKNOWN	not shown
plus `assert(a == b)`	2	PASS	none

Two 4-bit counters stepped together. The invariant fits on one line: a == b.

Asked in Interviews

Question	Answer
What is k-induction? What are the base case and the step?	Base: BMC from reset to depth k finds no failure. Step: k good states from anywhere are always followed by a good one. Both pass: proven.
Why did induction fail when BMC found no bug?	The step started in an unreachable state that satisfies the property and reaches a bad state. The property is not inductive.
What is a helper invariant and how do I find one?	An asserted, inductive fact about internal state that excludes those states. Read step 0 of the induction trace and write down what is impossible about it.

Try It

The lab runs fifo16 in prove mode at depth 12 with smtbmc yices. Measured: UNKNOWN, base case passed, induction failed.

Read the log
Find the basecase line and the induction line in the SBY summary. Then read step 0 of the trace. Could reset ever reach it?
Add the helpers
Add assert(count == wr_ptr - rd_ptr); and assert(count <= 5'd16); beside the property, set depth 2 and re-run.
Try depth instead
Remove the helpers and set depth 16. Read the verdict and the idle steps at the start of the trace.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module fifo16(input clk, rst, wr, rd, input [7:0] wdata,
  output [7:0] rdata, output empty, full);
  reg [7:0] mem [0:15];
  reg [4:0] wr_ptr=0, rd_ptr=0, count=0;
  assign empty = count == 5'd0;
  assign full  = count == 5'd16;
  wire do_wr = wr && !full, do_rd = rd && !empty;
  assign rdata = mem[rd_ptr[3:0]];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (do_wr) begin mem[wr_ptr[3:0]] <= wdata; wr_ptr <= wr_ptr + 5'd1; end
      if (do_rd) rd_ptr <= rd_ptr + 5'd1;
      count <= count + do_wr - do_rd;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);
  end
endmodule

Check Yourself

Predict the outputfifo16, no helpers, mode prove, depth 12, smtbmc yices, reset assumed in step 0. The verdict is:

module fifo16(input clk, rst, wr, rd, input [7:0] wdata,
  output [7:0] rdata, output empty, full);
  reg [7:0] mem [0:15];
  reg [4:0] wr_ptr=0, rd_ptr=0, count=0;
  assign empty = count == 5'd0;
  assign full  = count == 5'd16;
  wire do_wr = wr && !full, do_rd = rd && !empty;
  assign rdata = mem[rd_ptr[3:0]];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (do_wr) begin mem[wr_ptr[3:0]] <= wdata; wr_ptr <= wr_ptr + 5'd1; end
      if (do_rd) rd_ptr <= rd_ptr + 5'd1;
      count <= count + do_wr - do_rd;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);
  end
endmodule

ConceptWhich line should you not add to close the proof?

assert(count <= 5'd16);A larger depth, as an experimentassume(count == wr_ptr - rd_ptr);assert(count == wr_ptr - rd_ptr);

ConceptThe induction trace starts with count = 1, wr_ptr = 0, rd_ptr = 15. What does it tell you?

The solver is wrong, so the same task should be run again on another SMT solver.The RTL has a bug, and a base case with a larger depth would report it as a FAIL.The FIFO is too deep for formal; reduce it to four entries before trying again.The state is unreachable and the property is not inductive; add an invariant that excludes it.

Read the waveformWhich step-0 values in this induction trace could no reachable state have?