ASIC Point Explore

A FIFO, End to End

Build the complete formal bench for a FIFO: a two-entry scoreboard for order and integrity, the glue invariants, covers, a fault matrix and two routes to a proof.

Lesson
F8.1
Time
25 min
Runs on
SymbiYosys
Check
5 questions

A FIFO had passed a constrained-random bench with data checking for a year. A new consumer read and wrote at exactly the right moments, and data came out in the wrong order once every few million transactions. The write pointer wrapped at the slot count while the read pointer wrapped at the depth. A formal order check finds it in seven steps.

Spec sentenceKindBench line (Imm form)
Nothing is lost or changed: the tracked entry comes out with its dataend-to-endif (f_chk1) assert(read_valid && read_data == f_d1)
Data leaves in the order it enteredend-to-endif (f_chk2) assert(read_valid && read_data == f_d2)
full and empty tell the truth; the count never passes DEPTHglueassert(used <= DEPTH), assert(full == (used == DEPTH) ...)
The pointers stay in range and agree with the countglueassert(wp < DEPTH && rp < DEPTH), the pointer relation
read_valid only after an accepted readend-to-endassert(read_valid == f_tr)
The FIFO fills, a write and read meet at full, it drainscoverscover(full), cover(full && write_en && read_en), a fill-and-drain tracker

The plan before the code (F7.5): each sentence is one property or one cover. fifo_f has 48 flops.

A Scoreboard of Two

Two Tracked Writes Stand for Every PairThe solver picks any accepted write as the first; the next accepted write is the second. The bench copies their data and counts the entries in front of the first.
Two tracked writes stand for every pairThe solver picks any accepted write as the first; the next accepted write is the second. The bench copies their data and counts the entries in front of the first. component write side write_en, write_data component first: f_d1 any accepted write,chosen by the freeinput f_pick; f_aheadentries in front component second: f_d2 the very nextaccepted write component read side read_valid, read_dataone cycle after anaccepted read component checks f_d1 leaves whenf_ahead reaches 0;f_d2 is the very nextread f_ahead reads later
Read the diagram as text
  • write side: write_en, write_data
  • first: f_d1: any accepted write, chosen by the free input f_pick; f_ahead entries in front
  • second: f_d2: the very next accepted write
  • read side: read_valid, read_data one cycle after an accepted read
  • checks: f_d1 leaves when f_ahead reaches 0; f_d2 is the very next read
  • write side → first: f_d1
  • write side → second: f_d2
  • first: f_d1 → read side: f_ahead reads later
  • second: f_d2 → checks
  • read side → checks

The choice is free, so the proof covers every pair of consecutive entries with every data value (F4.4). Two in order, for every pair, is the whole sequence in order.

Formal does not store every packet. It tracks two consecutive accepted writes that the solver may pick anywhere, copies their data, and counts the entries in front of the first. When the count reaches zero the next read must return the first value, and the read after it the second.

One tracked value proves integrity: nothing lost, nothing changed. It cannot tell whether an older entry jumped the queue. Order needs the second.

This FIFO refuses a write when full and a read when empty, so it needs no input assumption. A FIFO without those guards needs assume(!(write_en && full)) from its producer, written down in the sign-off.

The Fault Matrix

BUG_PTR: the write pointer reaches a slot the reader never visits
01234567clkfreewrite_enfreeread_enfreewrite_data004C084C0C00wp01230rp01201usedread_data004C084Cf_d2000Cwp = 3read_data is not f_d2reported step 7

Measured with smtbmc yices: FAIL at reported step 7, 0.6 s. The write at step 4 lands in slot 3; the next read takes stale slot 0.

Fault (one line changed)Order pairCount gluePointer glueValid
BUG_PTR: A8.1 fault 6, wp wraps at fourFAIL, step 7BMC PASS to 12FAIL, step 5BMC PASS to 12
BUG_OVF: a write accepted when fullFAIL, step 7FAIL, step 6FAIL, step 6BMC PASS to 12
A8.1 fault 2: read_valid never clearedBMC PASS to 12BMC PASS to 12BMC PASS to 12FAIL, step 5
A8.1 fault 4: every answer one cycle lateFAIL, step 4BMC PASS to 12BMC PASS to 12FAIL, step 4

Each cell is one bmc run at depth 12 with that property alone. Step = reported step.

Glue properties find pointer and count bugs early and point at the line. The order pair is the spec and catches what the glue cannot see, such as a late answer. Fault 2 escapes both and only the valid check sees it: every spec sentence needs its own line.

Two Routes to a Proof

Correct fifo_f, all propertiesMeasured result
bmc depth 10BMC PASS to depth 10, 0.6 s
bmc depth 20time limit (20 s), no verdict, 20.1 s
prove k = 12, glue onlyUNKNOWN at k = 12 (base case passed, induction step failed), 1.0 s
prove k = 1, glue and tracker helpersUNKNOWN at k = 1 (base case passed, induction step failed), 0.5 s
prove k = 2, glue and tracker helpersProve PASS (k = 2), 0.5 s
abc pdr, no helpersProve PASS (abc pdr), 1.3 s

smtbmc yices unless noted. A bounded run at depth 20 does not finish in the budget; both proofs take about a second.

The glue is not enough. The induction step starts with the second tracked value inside (f_out1 = 1, f_in2 = 1), one entry left, and slot 2 holding some other byte. The missing helpers tie the tracker to the memory: where each tracked byte sits, and that it is still there (F4.6). Helpers may read inside the design; the checks themselves stay at the ports.

PDR proves the same set with no helpers in 1.3 s. The rule from F4.7: PDR to get the proof, helpers to understand it and to keep it when the design grows.

Asked in Interviews

QuestionAnswer
End-to-end or glue for a FIFO?Both. The order and integrity pair is the spec; the count and pointer relations are the helpers and the fast bug finders.
How does a formal scoreboard work without storing every packet?Two tracked writes chosen freely by the solver, with modelling flops for their data and position. The proof covers every pair.
Why did induction fail on a correct FIFO?The step started in a state no reset reaches: the tracker and the memory disagree. Helpers that tie them together close it.

Try It

The lab task: prove with abc pdr. The twins run covers, k-induction with and without helpers, and the two bugs.
[options]
mode prove
[engines]
abc pdr
[script]
read_verilog -formal -sv design.sv
prep -top fifo_f
[files]
design.sv
The core of the set in concurrent SVA.
assert property (@(posedge clk) disable iff (rst) f_chk1 |-> read_valid && read_data == f_d1);
assert property (@(posedge clk) disable iff (rst) f_chk2 |-> read_valid && read_data == f_d2);
assert property (@(posedge clk) disable iff (rst) used <= DEPTH && full == (used == DEPTH) && empty == (used == 0));
assert property (@(posedge clk) disable iff (rst) read_valid == $past(take_r));
cover property (@(posedge clk) disable iff (rst) full && write_en && read_en);
The bench as the engine runs it: the tracker, the checks, the helpers and the covers.
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling code: two consecutive accepted writes, picked by the solver, and their data.
  wire f_pick = $anyseq;
  reg f_in1 = 0, f_in2 = 0, f_out1 = 0, f_done = 0, f_chk1 = 0, f_chk2 = 0;
  reg [1:0] f_ahead = 0;                  // entries in front of the first tracked one
  reg [WIDTH-1:0] f_d1 = 0, f_d2 = 0;
  reg f_tr = 0;                           // an accepted read last cycle
  always @(posedge clk)
    if (rst) begin f_in1 <= 0; f_in2 <= 0; f_out1 <= 0; f_done <= 0; f_chk1 <= 0; f_chk2 <= 0; f_tr <= 0; end
    else begin
      f_tr <= take_r; f_chk1 <= 0; f_chk2 <= 0;
      if (!f_in1 && !f_out1 && !f_done && take_w && f_pick) begin
        f_in1 <= 1; f_d1 <= write_data; f_ahead <= used - take_r;
      end else if ((f_in1 || f_out1) && !f_in2 && take_w) begin f_in2 <= 1; f_d2 <= write_data; end
      if (f_in1 && take_r) begin
        if (f_ahead == 0) begin f_in1 <= 0; f_out1 <= 1; f_chk1 <= 1; end
        else f_ahead <= f_ahead - 2'd1;
      end
      if (f_out1 && f_in2 && take_r) begin f_out1 <= 0; f_in2 <= 0; f_done <= 1; f_chk2 <= 1; end
    end
  reg [1:0] f_round = 0;   // 0 nothing yet, 1 was empty then full, 2 empty again after that
  always @(posedge clk) if (rst) f_round <= 0; else if (f_round == 0 && full) f_round <= 1; else if (f_round == 1 && empty) f_round <= 2;
  always @(posedge clk) if (!rst) begin
    if (f_chk1) assert(read_valid && read_data == f_d1);   // nothing lost, nothing changed
    if (f_chk2) assert(read_valid && read_data == f_d2);   // the next one comes next
    assert(used <= DEPTH);                                 // glue: the count
    assert(full == (used == DEPTH) && empty == (used == 0));
    assert(wp < DEPTH && rp < DEPTH);                      // glue: the pointers
    assert(used == (wp >= rp ? wp - rp : wp + DEPTH - rp) || used == DEPTH && wp == rp);
    assert(read_valid == f_tr);                            // valid only after an accepted read
    // helpers for k-induction: where the tracked data sits
    if (f_in1) assert(f_ahead < used && mem[rp + f_ahead >= DEPTH ? rp + f_ahead - DEPTH : rp + f_ahead] == f_d1);
    if (f_in1 && f_in2) assert(f_ahead + 3'd2 <= used && mem[rp + f_ahead + 1 >= DEPTH ? rp + f_ahead + 1 - DEPTH : rp + f_ahead + 1] == f_d2);
    if (f_in1 && !f_in2) assert(f_ahead + 2'd1 == used);
    if (f_out1 && f_in2) assert(used != 0 && mem[rp] == f_d2);
    if (f_out1 && !f_in2) assert(used == 0);
    if (f_chk1 || f_chk2) assert(f_tr);
    assert(!(f_in1 && f_out1) && !(f_done && (f_in1 || f_out1 || f_in2)) && (!f_in2 || f_in1 || f_out1));
    c_full: cover(full);
    c_full_rw: cover(full && write_en && read_en);
    c_round: cover(f_round == 2'd2 && empty);
  end

  1. Wiggle

    Run the cover twin: full at step 5, a write and a read at full at step 5, fill and drain at step 9. Read each trace.

  2. Induction

    Run k = 12 without helpers, read step 0 of the induction trace, then switch the helpers on and run k = 2.

  3. Faults

    Run both bug twins and fill the matrix for the properties each one breaks.

  4. Sign off

    Write the line: which engine proved which set, with which helpers, under no input assumption.

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

    
Check Yourself

      

        
Predict the outputThe correct fifo_f, all properties without the tracker helpers, mode prove, k = 12, smtbmc yices, reset assumed in step 0. The verdict is:
      
module fifo_f #(parameter DEPTH = 3, WIDTH = 8)(input clk, rst, write_en, read_en,
  input [WIDTH-1:0] write_data, output full, empty, read_valid, output [WIDTH-1:0] read_data);
  reg [WIDTH-1:0] mem [0:3];                    // four slots, as A8.1
  reg [WIDTH-1:0] resp = 0, late_data = 0;
  reg resp_valid = 0, late_valid = 0;
  reg [1:0] wp = 0, rp = 0;
  reg [2:0] used = 0;
  wire take_w = write_en && used < DEPTH;
  wire take_r = read_en && used > 0;
  assign full = used == DEPTH;
  assign empty = used == 0;
  assign read_valid = resp_valid;
  assign read_data = resp;
  always @(posedge clk)
    if (rst) begin used <= 0; wp <= 0; rp <= 0; resp_valid <= 0; late_valid <= 0; end
    else begin
      late_valid <= resp_valid;
      if (resp_valid) late_data <= resp;
      resp_valid <= take_r;
      if (take_r) begin resp <= mem[rp]; rp <= rp == DEPTH - 1 ? 2'd0 : rp + 2'd1; end
      if (take_w) begin
        mem[wp] <= write_data;
        wp <= wp == DEPTH - 1 ? 2'd0 : wp + 2'd1;
      end
      used <= used + take_w - take_r;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling code: two consecutive accepted writes, picked by the solver, and their data.
  wire f_pick = $anyseq;
  reg f_in1 = 0, f_in2 = 0, f_out1 = 0, f_done = 0, f_chk1 = 0, f_chk2 = 0;
  reg [1:0] f_ahead = 0;                  // entries in front of the first tracked one
  reg [WIDTH-1:0] f_d1 = 0, f_d2 = 0;
  reg f_tr = 0;                           // an accepted read last cycle
  always @(posedge clk)
    if (rst) begin f_in1 <= 0; f_in2 <= 0; f_out1 <= 0; f_done <= 0; f_chk1 <= 0; f_chk2 <= 0; f_tr <= 0; end
    else begin
      f_tr <= take_r; f_chk1 <= 0; f_chk2 <= 0;
      if (!f_in1 && !f_out1 && !f_done && take_w && f_pick) begin
        f_in1 <= 1; f_d1 <= write_data; f_ahead <= used - take_r;
      end else if ((f_in1 || f_out1) && !f_in2 && take_w) begin f_in2 <= 1; f_d2 <= write_data; end
      if (f_in1 && take_r) begin
        if (f_ahead == 0) begin f_in1 <= 0; f_out1 <= 1; f_chk1 <= 1; end
        else f_ahead <= f_ahead - 2'd1;
      end
      if (f_out1 && f_in2 && take_r) begin f_out1 <= 0; f_in2 <= 0; f_done <= 1; f_chk2 <= 1; end
    end
  always @(posedge clk) if (!rst) begin
    if (f_chk1) assert(read_valid && read_data == f_d1);   // nothing lost, nothing changed
    if (f_chk2) assert(read_valid && read_data == f_d2);   // the next one comes next
    assert(used <= DEPTH);                                 // glue: the count
    assert(full == (used == DEPTH) && empty == (used == 0));
    assert(wp < DEPTH && rp < DEPTH);                      // glue: the pointers
    assert(used == (wp >= rp ? wp - rp : wp + DEPTH - rp) || used == DEPTH && wp == rp);
    assert(read_valid == f_tr);                            // valid only after an accepted read
  end
`endif
endmodule


      

      

      


ConceptWhich line is the wrong one for this bench?


ConceptWhy do two freely chosen tracked writes prove order for every pair of entries?


Read the waveformIn the BUG_PTR trace, at which step does wp leave the range 0 to 2, and at which step is the order failure reported?
BUG_PTR: the write pointer reaches a slot the reader never visits

    
  01234567clkfreewrite_enfreeread_enfreewrite_data004C084C0C00wp01230rp01201usedread_data004C084Cf_d2000Cwp = 3read_data is not f_d2reported step 7
Measured with smtbmc yices: FAIL at reported step 7, 0.6 s. The write at step 4 lands in slot 3; the next read takes stale slot 0.


Predict the outputfifo_f with A8.1 fault 2 (read_valid never cleared), only the order pair, mode bmc, depth 12, smtbmc yices. The verdict is:
      
module fifo_f #(parameter DEPTH = 3, WIDTH = 8)(input clk, rst, write_en, read_en,
  input [WIDTH-1:0] write_data, output full, empty, read_valid, output [WIDTH-1:0] read_data);
  reg [WIDTH-1:0] mem [0:3];                    // four slots, as A8.1
  reg [WIDTH-1:0] resp = 0, late_data = 0;
  reg resp_valid = 0, late_valid = 0;
  reg [1:0] wp = 0, rp = 0;
  reg [2:0] used = 0;
  wire take_w = write_en && used < DEPTH;
  wire take_r = read_en && used > 0;
  assign full = used == DEPTH;
  assign empty = used == 0;
  assign read_valid = resp_valid;
  assign read_data = resp;
  always @(posedge clk)
    if (rst) begin used <= 0; wp <= 0; rp <= 0; resp_valid <= 0; late_valid <= 0; end
    else begin
      late_valid <= resp_valid;
      if (resp_valid) late_data <= resp;
      if (take_r) resp_valid <= 1;   // fault 2: never cleared
      if (take_r) begin resp <= mem[rp]; rp <= rp == DEPTH - 1 ? 2'd0 : rp + 2'd1; end
      if (take_w) begin
        mem[wp] <= write_data;
        wp <= wp == DEPTH - 1 ? 2'd0 : wp + 2'd1;
      end
      used <= used + take_w - take_r;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling code: two consecutive accepted writes, picked by the solver, and their data.
  wire f_pick = $anyseq;
  reg f_in1 = 0, f_in2 = 0, f_out1 = 0, f_done = 0, f_chk1 = 0, f_chk2 = 0;
  reg [1:0] f_ahead = 0;                  // entries in front of the first tracked one
  reg [WIDTH-1:0] f_d1 = 0, f_d2 = 0;
  reg f_tr = 0;                           // an accepted read last cycle
  always @(posedge clk)
    if (rst) begin f_in1 <= 0; f_in2 <= 0; f_out1 <= 0; f_done <= 0; f_chk1 <= 0; f_chk2 <= 0; f_tr <= 0; end
    else begin
      f_tr <= take_r; f_chk1 <= 0; f_chk2 <= 0;
      if (!f_in1 && !f_out1 && !f_done && take_w && f_pick) begin
        f_in1 <= 1; f_d1 <= write_data; f_ahead <= used - take_r;
      end else if ((f_in1 || f_out1) && !f_in2 && take_w) begin f_in2 <= 1; f_d2 <= write_data; end
      if (f_in1 && take_r) begin
        if (f_ahead == 0) begin f_in1 <= 0; f_out1 <= 1; f_chk1 <= 1; end
        else f_ahead <= f_ahead - 2'd1;
      end
      if (f_out1 && f_in2 && take_r) begin f_out1 <= 0; f_in2 <= 0; f_done <= 1; f_chk2 <= 1; end
    end
  always @(posedge clk) if (!rst) begin
    if (f_chk1) assert(read_valid && read_data == f_d1);   // nothing lost, nothing changed
    if (f_chk2) assert(read_valid && read_data == f_d2);   // the next one comes next
  end
`endif
endmodule


      

      

      

        

        
      

    

    
Remember
  • Write the spec sentences first; each becomes one property or one cover.
  • Two freely chosen tracked writes check integrity and order for every pair.
  • Glue finds pointer bugs fast; end-to-end checks find what glue cannot; a fault matrix shows the gaps.
  • Induction needs helpers that tie the tracker to the memory; PDR finds its own invariant.