Counter, Memory and Parameter Abstraction

A Counter Is Mostly Waiting

The design acts on two counter values; everything between them is waiting. Each extra bit doubles the wait, and PDR’s time grows with it. The abstraction has five states at any width: Prove PASS, 0.5 s, and the cover of up is reached at step 7.

A plain cut forgets the order: at_last may come before at_cal, and up rises with no calibration. That failure is false. The abstraction keeps the order and lets the solver choose how long each wait lasts, which covers every real timing.

Prove the Abstraction Is Faithful

assert(region(cnt) == r_q || region(cnt) == r_q + 3'd1);   // stay, or step to the next region
if (r_q == 3'd0 || r_q == 3'd2) assert(region(cnt) == r_q + 3'd1);   // ZERO and AT_CAL last one cycle

An abstraction is an assumption in disguise, so justify it on the real logic. The side run proves that the counter’s region only stays or steps to the next one, and that ZERO and AT_CAL last one cycle. It is inductive at once, so 16 bits cost nothing.

With the side proof, every real trace is a trace of the abstract model, so a PASS there holds for the real design. The faulty twin fails on both, and the abstract counterexample is short enough to read.

Ask three questions of every abstraction. Does it admit every real behaviour? Which properties changed meaning? Can the abstract element still do what the properties need? The cover answers the third; without it, an abstraction is an over-constraint waiting to be found.

Shrink a Parameter

A reduced parameter is sound when the small design is the large one, scaled. A constant written for one size breaks that: the count here is 3 bits wide, enough for depth 4. At depth 4 the proof passes; at depth 64 the count wraps after 8 words and bmc fails at step 10.

Prove at the reduced size, then check the full size by bmc or by coverage: every line reachable in the full design must be reachable in the reduced one. Memories reduce the same way, to one tracked row at a symbolic address, as the F4.4 tracker does for a FIFO.

Asked in Interviews

Try It

The lab is pfifo at depth 4 under abc pdr. Measured: Prove PASS, 0.5 s. The twins include the wake counter, its abstraction and the side proof.

assert property (@(posedge clk) disable iff (rst) up |-> cal_done);

1. Scale the parameter

   Set DEPTH to 16 (pointers 5 bits, count 5 bits) and compare the time with depth 4.

2. Hide a bug

   Make the count 3 bits wide at depth 4 and prove it; then set depth 64 and run bmc at depth 20.

3. Abstract the counter

   In phy_wake, replace the counter with the five-state model and run abc pdr; then cut both decodes to $anyseq and read the false trace.

Check Yourself

module phy_wake(input clk, rst, cal_ok, output reg up = 0, output reg cal_done = 0);
  wire at_cal = $anyseq, at_last = $anyseq;   // the counter cut away
  always @(posedge clk)
    if (rst) begin up <= 0; cal_done <= 0; end
    else begin
      if (at_cal) cal_done <= 1;
      if (at_last) up <= 1;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    if (up) assert(cal_done);
    cover(up);
  end
endmodule

module pfifo(input clk, rst, wr, rd, input [7:0] wdata, output [7:0] rdata, output empty, full);
  localparam DEPTH = 64;
  reg [7:0] mem [0:DEPTH-1];
  reg [6:0] wr_ptr = 0, rd_ptr = 0;
  reg [2:0] count = 0;   // written for the 4-deep build
  assign empty = count == 0;
  assign full = count == DEPTH;
  wire do_wr = wr && !full, do_rd = rd && !empty;
  assign rdata = mem[rd_ptr[5: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[5:0]] <= wdata; wr_ptr <= wr_ptr + 1'b1; end
      if (do_rd) rd_ptr <= rd_ptr + 1'b1;
      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);
    if (full) assert(wr_ptr[5:0] == rd_ptr[5:0] && wr_ptr != rd_ptr);
  end
endmodule