Symbolic Constants and Data Independence: The Formal Scoreboard

Check a FIFO end to end with one symbolic packet instead of a reference queue, see why one value covers every value, and spot the design that reads its data and breaks the argument.

Lesson: F4.4
Time: 25 min
Runs on: SymbiYosys
Check: 5 questions

The FIFO’s scoreboard kept a copy of every word, like a simulation testbench. At 8 entries of 8 bits it proved in 4.0 s; at 32-bit data or 16 entries it ran out of time. The formal scoreboard that replaced it follows one packet and proves the 16 × 32 FIFO in 0.5 s.

Follow One Packet

One Symbolic Packet Through the FIFOThe solver picks a value and an entry time. The tracker follows that one packet from its write to its read.

Read the diagram as text

f_val = $anyconst: one value, fixed for the run, any value
f_pick = $anyseq: free each cycle: which write to follow
enters: records its slot and the words ahead
waits: each read lowers the words ahead
at the head: assert: rdata == f_val
while inside: assert: the FIFO is not empty

f_val = $anyconst → enters: wdata == f_val
f_pick = $anyseq → enters
enters → waits
waits → at the head: none ahead
waits → while inside

A drop, duplicate, reorder or corruption breaks one of the two assertions for some choice of packet.

The tracker watches one packet. f_val is an $anyconst: a single value, fixed for the run, that the solver chooses. f_pick is free in every cycle, so the packet may enter at any write. A PASS therefore covers every value at every entry time at once.

The tracker remembers	Why
`f_in`, `f_done`	the packet is inside; it has left (track it once)
`f_addr`	the slot it was written to
`f_ahead`	words in front of it; it must come out when this reaches 0

Three small registers replace a copy of every word.

Two assertions carry the whole end-to-end check: while the packet is inside, the FIFO is not empty, and when it reaches the head it comes out unchanged. A local variable in a simulation assertion does the same job per attempt (A4.1 Local variables); here one symbolic attempt stands for all of them.

The same idea on a memory is a symbolic address: one $anyconst address and one shadow word, checking that a read of that address returns the last write to it.

Tracker Against Reference Queue

Check	Depth × width	Measured result
reference queue, `abc pdr`	8 × 8	Prove PASS, 4.0 s
reference queue, `abc pdr`	8 × 32	time limit (20 s), no verdict
reference queue, `abc pdr`	16 × 8	time limit (20 s), no verdict
tracker, no helpers, prove 8	8 × 8	UNKNOWN at depth 8, 0.5 s
tracker with helpers, prove 2	8 × 8	Prove PASS, 0.5 s
tracker with helpers, prove 2	16 × 32	Prove PASS, 0.5 s
tracker with helpers, prove 2	8 × 2	Prove PASS, 0.5 s

Prove runs use smtbmc yices. The helpers are assertions, so they are proven too. Flop bits at 8 × 8 after prep: 16 with the reference queue, 18 with the tracker.

The reference queue doubles the memory, and a proof must relate every slot of one memory to the same slot of the other. The tracker relates one slot. Its helpers say where the packet sits and that its slot still holds f_val, which makes the check inductive at depth 2 for every size here.

The four helpers. Without them k-induction stays UNKNOWN. With them, depth 1 is not enough either: UNKNOWN at depth 1, 0.5 s.

assert(used <= 8);
assert(f_dist == f_ahead);
assert(f_ahead < used);
assert(mem[f_addr[2:0]] == f_val);

Data Independence, and Where It Stops

Stores and moves words only

wire do_wr = wr && !full, do_rd = rd && !empty;

2-bit words: Prove PASS, 0.5 s. 32-bit: Prove PASS, 0.5 s.

Reads its data

wire do_wr = wr && !full
  && !(wdata == 8'hFF && last_ff);

8-bit: FAIL at step 4, 0.5 s. 2-bit: Prove PASS, 0.5 s.

A design is data independent when no decision reads the data: words are only stored and moved. Values then cannot steer control, so a proof with 2-bit words carries over to 32 bits (Wolper, 1986). The 2-bit and 32-bit runs agree, as the argument predicts.

Measured counterexample of the fill-word FIFO at 8 bits (bmc, depth 12): FAIL at step 4, 0.5 s. The solver chose f_val = 255.

The fill-word FIFO drops a second 8'hFF in a row. It reads its data, so the reduction is off: at 8 bits the solver sets f_val = 255 and the packet vanishes; at 2 bits the constant can never occur and the bug disappears. The full-width tracker still finds it, so keep the real width when the data steers control.

Faulty FIFO, tracker with helpers	Measured result
drops a second fill word, 8 bits, `bmc` 12	FAIL at step 4, 0.5 s
same, 2-bit words, prove 2	Prove PASS, 0.5 s
reads the neighbouring slot, 8 bits, `bmc` 12	FAIL at step 3, 0.5 s
one pop does not advance (a word comes out twice), 8 bits, `bmc` 12	FAIL at step 5, 0.5 s

Soundness twins: the tracker catches the drop, the reorder and the duplicate at full width.

Asked in Interviews

Question	Answer
How does a formal scoreboard work without storing every packet?	It follows one symbolic packet: an `$anyconst` value entering at a solver-chosen write. Assert it is never lost and leaves first in line, unchanged. Because the choice is free, one proof covers every packet.
What is data independence?	The design never branches on data values; it only stores and moves them. Then a narrow data width proves the wide one. It fails as soon as control compares data with a constant.
What is a symbolic constant?	A value chosen once by the solver and held for the run (`$anyconst`, a rigid free variable). It turns "for every address" or "for every packet" into one proof.

Try It

The lab is the 8 × 8 FIFO with the tracker and its helpers, prove depth 2, smtbmc yices. Measured: Prove PASS, 0.5 s.

The two end-to-end rules in concurrent SVA.

assert property (@(posedge clk) disable iff (rst) f_in |-> !empty);
assert property (@(posedge clk) disable iff (rst) f_in && f_ahead == 0 |-> rdata == f_val);

Widen it
Set the data to 32 bits and the depth to 16 (change the widths, the memory size and the constant 8 in the helpers) and run again.
Remove a helper
Delete assert(mem[f_addr[2:0]] == f_val); and read the induction trace: what does the tracked slot hold at step 0?
Break the FIFO
Make the read use mem[rd_ptr[2:0] ^ 1'b1] and run bmc at depth 12.

Top moduleModeDepthEngine

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

Enable JavaScript to edit and run. The original design and properties follow.

module sfifo(input clk, rst, wr, rd, input [7:0] wdata, output [7:0] rdata, output empty, full);
  reg [7:0] mem [0:7];
  reg [3:0] wr_ptr = 0, rd_ptr = 0;
  wire [3:0] used = wr_ptr - rd_ptr;
  assign empty = used == 0;
  assign full = used == 8;
  assign rdata = mem[rd_ptr[2:0]];
  wire do_wr = wr && !full, do_rd = rd && !empty;
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; end
    else begin
      if (do_wr) begin mem[wr_ptr[2:0]] <= wdata; wr_ptr <= wr_ptr + 1'b1; end
      if (do_rd) rd_ptr <= rd_ptr + 1'b1;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // one symbolic packet: any value, entering at any accepted write the solver picks
  wire [7:0] f_val = $anyconst;
  wire f_pick = $anyseq;
  reg f_in = 0, f_done = 0;
  reg [3:0] f_addr = 0;       // the slot it was written to
  reg [3:0] f_ahead = 0;      // words in front of it
  wire f_enter = !f_in && !f_done && wr && !full && f_pick && wdata == f_val;
  always @(posedge clk)
    if (rst) begin f_in <= 0; f_done <= 0; end
    else if (f_enter) begin f_in <= 1; f_addr <= wr_ptr; f_ahead <= used - do_rd; end
    else if (f_in && do_rd) begin
      if (f_ahead == 0) begin f_in <= 0; f_done <= 1; end
      else f_ahead <= f_ahead - 1'b1;
    end
  always @(posedge clk) if (!rst && f_in) begin
    assert(!empty);                              // never dropped
    if (f_ahead == 0) assert(rdata == f_val);     // leaves first in line, unchanged
  end
  // helpers: where the tracked word sits, and that it is still there
  wire [3:0] f_dist = f_addr - rd_ptr;
  always @(posedge clk) if (!rst) begin
    assert(used <= 8);
    if (f_in) begin
      assert(f_dist == f_ahead);
      assert(f_ahead < used);
      assert(mem[f_addr[2:0]] == f_val);
    end
  end
endmodule

Check Yourself

Predict the outputThe 8 × 8 FIFO with the tracker and all four helpers, mode prove, depth 1, smtbmc yices, reset assumed in step 0. The verdict is:

module sfifo(input clk, rst, wr, rd, input [7:0] wdata, output [7:0] rdata, output empty, full);
  reg [7:0] mem [0:7];
  reg [3:0] wr_ptr = 0, rd_ptr = 0;
  wire [3:0] used = wr_ptr - rd_ptr;
  assign empty = used == 0;
  assign full = used == 8;
  assign rdata = mem[rd_ptr[2:0]];
  wire do_wr = wr && !full, do_rd = rd && !empty;
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; end
    else begin
      if (do_wr) begin mem[wr_ptr[2:0]] <= wdata; wr_ptr <= wr_ptr + 1'b1; end
      if (do_rd) rd_ptr <= rd_ptr + 1'b1;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // one symbolic packet: any value, entering at any accepted write the solver picks
  wire [7:0] f_val = $anyconst;
  wire f_pick = $anyseq;
  reg f_in = 0, f_done = 0;
  reg [3:0] f_addr = 0;       // the slot it was written to
  reg [3:0] f_ahead = 0;      // words in front of it
  wire f_enter = !f_in && !f_done && wr && !full && f_pick && wdata == f_val;
  always @(posedge clk)
    if (rst) begin f_in <= 0; f_done <= 0; end
    else if (f_enter) begin f_in <= 1; f_addr <= wr_ptr; f_ahead <= used - do_rd; end
    else if (f_in && do_rd) begin
      if (f_ahead == 0) begin f_in <= 0; f_done <= 1; end
      else f_ahead <= f_ahead - 1'b1;
    end
  always @(posedge clk) if (!rst && f_in) begin
    assert(!empty);                              // never dropped
    if (f_ahead == 0) assert(rdata == f_val);     // leaves first in line, unchanged
  end
  // helpers: where the tracked word sits, and that it is still there
  wire [3:0] f_dist = f_addr - rd_ptr;
  always @(posedge clk) if (!rst) begin
    assert(used <= 8);
    if (f_in) begin
      assert(f_dist == f_ahead);
      assert(f_ahead < used);
      assert(mem[f_addr[2:0]] == f_val);
    end
  end
endmodule

Predict the outputThe fill-word FIFO with 2-bit data, tracker and helpers, mode prove, depth 2, smtbmc yices. The verdict is:

module sfifo(input clk, rst, wr, rd, input [1:0] wdata, output [1:0] rdata, output empty, full);
  reg [1:0] mem [0:7];
  reg [3:0] wr_ptr = 0, rd_ptr = 0;
  wire [3:0] used = wr_ptr - rd_ptr;
  assign empty = used == 0;
  assign full = used == 8;
  assign rdata = mem[rd_ptr[2:0]];
  reg last_ff = 0;   // fill-word compression: a second 8'hFF in a row is not stored
  always @(posedge clk) if (rst) last_ff <= 0; else if (wr && !full) last_ff <= wdata == 8'hFF;
  wire do_wr = wr && !full && !(wdata == 8'hFF && last_ff), do_rd = rd && !empty;
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; end
    else begin
      if (do_wr) begin mem[wr_ptr[2:0]] <= wdata; wr_ptr <= wr_ptr + 1'b1; end
      if (do_rd) rd_ptr <= rd_ptr + 1'b1;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // one symbolic packet: any value, entering at any accepted write the solver picks
  wire [1:0] f_val = $anyconst;
  wire f_pick = $anyseq;
  reg f_in = 0, f_done = 0;
  reg [3:0] f_addr = 0;       // the slot it was written to
  reg [3:0] f_ahead = 0;      // words in front of it
  wire f_enter = !f_in && !f_done && wr && !full && f_pick && wdata == f_val;
  always @(posedge clk)
    if (rst) begin f_in <= 0; f_done <= 0; end
    else if (f_enter) begin f_in <= 1; f_addr <= wr_ptr; f_ahead <= used - do_rd; end
    else if (f_in && do_rd) begin
      if (f_ahead == 0) begin f_in <= 0; f_done <= 1; end
      else f_ahead <= f_ahead - 1'b1;
    end
  always @(posedge clk) if (!rst && f_in) begin
    assert(!empty);                              // never dropped
    if (f_ahead == 0) assert(rdata == f_val);     // leaves first in line, unchanged
  end
  // helpers: where the tracked word sits, and that it is still there
  wire [3:0] f_dist = f_addr - rd_ptr;
  always @(posedge clk) if (!rst) begin
    assert(used <= 8);
    if (f_in) begin
      assert(f_dist == f_ahead);
      assert(f_ahead < used);
      assert(mem[f_addr[2:0]] == f_val);
    end
  end
endmodule

ConceptWhy does one tracked packet prove the property for every packet?

Its value and entry time are free choices of the solver.The FIFO is small enough to try every value.The tracker stores a copy of every packet written.Induction at depth 2 checks every value one by one.

ConceptFor which design does a 2-bit proof not carry over to 32 bits?

A skid buffer in front of a ready signalA FIFO that discards words equal to an idle codeA pipeline register stage with a valid bitA FIFO that stores and forwards words unchanged

Read the waveformIn the measured fill-word trace, what happens to the tracked packet?

Measured counterexample of the fill-word FIFO at 8 bits (bmc, depth 12): FAIL at step 4, 0.5 s. The solver chose f_val = 255.

It is stored, but corrupted on its way through the memory.It is read twice by two back-to-back reads of the head.It is a second 8'hFF in a row and is never stored.It enters while the FIFO is already full and is lost.

Remember

A formal scoreboard tracks one symbolic packet: $anyconst value, free entry time.
Two assertions (never lost, leaves first and unchanged) replace a reference queue.
Helpers about the tracked slot make it inductive at small depth.
Data width can be reduced only when no control reads the data.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.