Lesson 10.4 · Taming Complexity

Abstracting counters and memories

Counter abstraction

A watchdog counts to 2²⁰ before firing. Any property about what happens after the timeout needs a million cycles of BMC — hopeless. But most properties do not care about the exact count, only about "the timeout can happen at some point after start". Replace the counter with a free signal that is constrained just enough:

watchdog.sv

// watchdog.sv — FSM with a large timeout counter
module watchdog #(
  parameter int TW = 20
) (
  input  logic clk, rst, start, kick, stop,
  output logic bark                       // timeout expired
);
  typedef enum logic [1:0] {OFF, ARMED, BARK} st_t;
  st_t         st;
  logic [TW-1:0] cnt;
  logic        expired;

  assign expired = (cnt == '1);           // all ones = timeout
  assign bark    = (st == BARK);

  always_ff @(posedge clk) begin
    if (rst) begin
      st  <= OFF;
      cnt <= '0;
    end else begin
      case (st)
        OFF:     if (start) begin st <= ARMED; cnt <= '0; end
        ARMED:   if (stop)         st  <= OFF;
                 else if (kick)    cnt <= '0;
                 else if (expired) st  <= BARK;
                 else              cnt <= cnt + 1'b1;
        BARK:    if (stop)         st  <= OFF;
        default: st <= OFF;
      endcase
    end
  end
endmodule

The abstraction: make expired a cut point, so it can be 1 on any cycle. That over-approximates the real counter (the real one only expires after 2²⁰ quiet cycles), so safety proofs remain sound. Properties about the FSM now prove at small depth:

watchdog_fv.sv

// watchdog_fv.sv — properties that do not depend on the exact count
module watchdog_fv (input logic clk, rst, start, kick, stop);
  logic bark;
  watchdog #(.TW(20)) dut (.*);

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

  // BARK is only entered from a quiet ARMED cycle (no stop, no kick)
  a_bark_quiet:     assert property ($rose(bark) |-> $past(!stop && !kick));
  a_stop_silences:  assert property (stop |=> !bark);
  a_bark_sticky:    assert property (bark && !stop |=> bark);
  c_bark:           cover  property (bark);   // with the cut: a few cycles; without: ~2^20
endmodule
// Tool command (vendor-specific), e.g.:  cut  dut.expired   /  stopat dut.expired

Properties that do depend on the count ("bark exactly 2²⁰ cycles after the last kick") need a different approach: reduce TW to a small value in a separate run and argue that the counter logic is width-independent.

Memory abstraction

A 64 KB memory has half a million state bits. For most control properties, the memory contents are irrelevant except at one location — the one a property cares about. A common abstraction keeps only one symbolic address:

Choose a free but stable address sym_addr (an input with assume property ($stable(sym_addr))).
Model a single data register that is written when wr_addr == sym_addr.
Reads from sym_addr return the modelled data; reads from other addresses return free values.

Because sym_addr can be any address, a property proven for it holds for all addresses — the same "track one arbitrary item" idea as the FIFO in Chapter 6.