Lesson 1.2 · Welcome to Formal Verification

Your first formal bug hunt

Let us make this concrete with a design small enough to read in ten seconds. A credit counter keeps track of how many buffer slots a downstream block has free. It increments when a slot is returned (inc) and decrements when a slot is used (dec). It should never exceed MAX and never go below zero.

credit_counter.sv

// credit_counter.sv — tracks free buffer credits (contains a deliberate bug)
module credit_counter #(
  parameter int MAX = 12
) (
  input  logic       clk,
  input  logic       rst,       // synchronous, active-high
  input  logic       inc,       // a credit is returned
  input  logic       dec,       // a credit is consumed
  output logic [3:0] credits
);
  always_ff @(posedge clk) begin
    if (rst) begin
      credits <= 4'(MAX);           // all slots free after reset
    end else begin
      case ({inc, dec})
        2'b10:   if (credits != 4'(MAX)) credits <= credits + 4'd1;
        2'b01:   credits <= credits - 4'd1;    // BUG: no guard at zero
        default: credits <= credits;           // both or neither: no change
      endcase
    end
  end
endmodule

A typical directed test might reset the counter, consume a few credits, return them and check the value. Because a well-behaved testbench never consumes a credit it does not have, the bug at zero could survive for a long time. Let us instead state the requirement as an assertion and give it to a formal tool:

credit_counter_fv.sv

// credit_counter_fv.sv — formal wrapper with properties
module credit_counter_fv (
  input logic clk, rst, inc, dec    // top-level inputs are left FREE by the tool
);
  logic [3:0] credits;

  credit_counter #(.MAX(12)) dut (.*);

  // Every trace starts in reset (open-source flow; commercial tools use a reset command)
  initial assume (rst);

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

  // The requirement: credits stay in the legal range 0..MAX
  a_in_range: assert property (credits <= 4'd12);

  // Something we want to SEE: the counter reaching zero at all
  c_empty:    cover  property (credits == 4'd0);
endmodule

Notice what is missing: there is no stimulus. We never say "set dec to 1 for 12 cycles". The wrapper's inputs inc and dec are left free, so the tool considers every possible value on every cycle. In a fraction of a second it reports that a_in_range fails and shows a counterexample like this one:

Counterexample: after reset, consume a credit every cycle. One step past zero the 4-bit counter wraps to 15 and the assertion fails.

The waveform is the shortest path to the failure: thirteen consecutive dec pulses. Of course a real upstream block should never send dec when credits are zero — but is that guaranteed? Either the design must guard against it, or the environment must promise it. Formal forces you to make that decision explicitly.

Two ways to resolve the failure

Option A — fix the design so that it ignores an illegal dec:

fix in RTL

2'b01:   if (credits != 4'd0) credits <= credits - 4'd1;

Option B — record the interface rule as an assumption, if the specification says the upstream block must never consume credits it does not have:

environment assumption

// Legal environment: never consume a credit when none are available
m_no_underflow: assume property (credits == 4'd0 |-> !dec);

credit_counter.sby

# credit_counter.sby — SymbiYosys run script (see the Labs page)
[tasks]
prove
cover

[options]
prove: mode prove
cover: mode cover
depth 20

[engines]
smtbmc

[script]
read -formal credit_counter.sv credit_counter_fv.sv
prep -top credit_counter_fv

[files]
credit_counter.sv
credit_counter_fv.sv