IC3/PDR: Invariants Found by the Tool

Frames Instead of Copies

IC3 never unrolls. It keeps frames F0 to Fk. F0 is the initial states. Each later frame is a set of clauses, small lemmas about the state, that every state reachable in that many steps satisfies. Every frame excludes the bad states.

The Same FIFO, One Engine Line Changed

k-induction only has the property and a window of k states. PDR strengthens the property itself until it is inductive. Each clause it learns is a tiny helper invariant, proven relative to the frame before it. That is why it needs none from you on finite control logic.

The Invariant It Found

.i 18
.o 1
.p 220
---------------1-0 1
---------------11- 1
-------------11--- 1
------------1-1--- 1
-----------1--1--- 1
----------1---1--- 1
----0----0----1--- 1
----0----100000--- 1
...

Each row is one lemma over the latch bits: 0 or 1 where it tests a bit, - where it ignores one. The 18 bits are the two 5-bit pointers and the 5-bit count, two flops that sample the assertion, and the first-step latch. The memory is gone: no property reads it.

Your two helpers say the same thing in two lines. PDR says it in 220 bit-level lemmas. The count changes from run to run, because ABC's PDR uses internal time limits. In this run the log reached frame 36 and ended with "Proved output 0 in frame 1 (converged)."

Its Counterexamples Start at Reset

PDR reports a failure only after tracing a bad cube back to F0, so its traces are real counterexamples from reset. They need not be the shortest: on this bug PDR reported step 22, while BMC at depth 20 reported step 19.

Where It Shines, and Where It Stalls

PDR works on the bit-level AIGER. Wide arithmetic becomes thousands of gates, and there it can stall where word-level induction with a helper finishes quickly. F2.6 measures one such case.

Asked in Interviews

Try It

The lab runs fifo16 without helpers under abc pdr. Measured: PASS in 1.5 s.

1. Change one line

   Switch the engine to smtbmc yices, depth 12, and re-run: UNKNOWN. Switch back to abc pdr. What did the engine know that the window did not?

2. The engineer’s route

   Add the two F2.4 helpers and run smtbmc yices at depth 2. Compare the time with PDR’s.

3. Break a pointer

   Make rd_ptr wrap at 16: rd_ptr <= rd_ptr == 5'd15 ? 5'd0 : rd_ptr + 5'd1;. Run abc pdr and read step 0 of its trace.

Check Yourself

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