The Formal Scoreboard with One Symbolic Word

Where the interviewer goes next. Open a node to practise that follow-up.

WhyWhat IfProve ItCompareScale It

1. The Formal Scoreboard with One Symbolic Word
2. WhyWhy the Tracker Proof Needs HelpersL2 Mid-LevelL3 Senior

   Why does the symbolic tracker proof need helper assertions before k-induction (an induction proof over k steps) can close it?

   Reveal the Model Answer

   Without helpers the induction step may start with the tracker claiming a word is stored in a slot that holds something else. Helpers tie the tracker to the design. Its distance from the read pointer equals the count of words ahead. Memory at the tracked slot still holds the value. Without them the proof stays UNKNOWN even at k = 8; with them it closes at k = 2.

   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
   endmodule
   

   Prints: prove, depth 8 (smtbmc yices): UNKNOWN

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Without helpers the induction step may start with the tracker claiming a word is stored in a slot that holds something else. Key point 2 Helpers tie the tracker to the design. Key point 3 Its distance from the read pointer equals the count of words ahead. Key point 4 Memory at the tracked slot still holds the value. Key point 5 Without them the proof stays UNKNOWN even at k = 8; with them it closes at k = 2.

   • Lesson F4.4Symbolic Constants and Data Independence: The Formal Scoreboard
   • Lesson F8.1A FIFO, End to End
3. Prove ItSolve F4.4.1: Implement the Symbolic Packet TrackerSimulator-graded

   Show it, don't just say it: this Silicon Lab problem is graded by the simulator.

   Open Problem F4.4.1

4. What IfTwo Tracked Words for OrderingL2 Mid-Level

   What if you also want to check that two different words never swap order?

   Reveal the Model Answer

   Track two writes chosen freely by the solver, the first accepted before the second. Assert that the first leaves before the second and both arrive unchanged. Because both choices are free, the check covers every pair of words, which catches reordering that a single tracker cannot see.

   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 solver may pick any accepted write as the first, so the proof covers every pair of entries in a row.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Track two writes chosen freely by the solver, the first accepted before the second. Key point 2 Assert that the first leaves before the second and both arrive unchanged. Key point 3 Because both choices are free, the check covers every pair of words, which catches reordering that a single tracker cannot see.

   • Lesson F8.1A FIFO, End to End
   • Problem F8.1.1Sign off a Four-Entry FIFO
   • Problem F8.1.2Strengthen the FIFO Induction
5. Prove ItSolve F8.1.1: Sign off a Four-Entry FIFOSimulator-graded

   Show it, don't just say it: this Silicon Lab problem is graded by the simulator.

   Open Problem F8.1.1

6. WhyWhy Two Free Words Cover Every PairL2 Mid-LevelL3 Senior

   Why does choosing both words freely cover every pair, when the proof only ever tracks two?

   Reveal the Model Answer

   The solver may pick any two writes, at any times, as the tracked pair. A proof must hold for every choice it could make. So if any pair could swap, some choice of the two tracked words shows it. Two trackers then stand for all pairs, with only two sets of state.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 The solver may pick any two writes, at any times, as the tracked pair. Key point 2 A proof must hold for every choice it could make. Key point 3 So if any pair could swap, some choice of the two tracked words shows it. Key point 4 Two trackers then stand for all pairs, with only two sets of state.

   Misconception

   "Tracking two words only checks those two words."

   The words are free variables, so the proof covers every value the solver could choose. One run checks all pairs.

   Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 10 "Exploiting symmetry with rigid free variables"

   • Lesson F8.1A FIFO, End to End
   • Problem F8.1.1Sign off a Four-Entry FIFO
7. CompareSymbolic Tracker vs Reference QueueL2 Mid-LevelL3 Senior

   Asked if they propose a reference queue

   Compare a symbolic tracker with a reference-model queue as the scoreboard of a formal bench.

   Reveal the Model Answer

   A reference queue copies every word, so its state grows with depth times width. The solver must reason about all of it. The tracker holds one value, one slot and one count, yet covers every word through the free choice. The queue is closer to a simulation scoreboard and easier to read, so people pick it first. The tracker is what converges.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 A reference queue copies every word, so its state grows with depth times width. Key point 2 The solver must reason about all of it. Key point 3 The tracker holds one value, one slot and one count, yet covers every word through the free choice. Key point 4 The queue is closer to a simulation scoreboard and easier to read, so people pick it first. Key point 5 The tracker is what converges.

   • Lesson F4.4Symbolic Constants and Data Independence: The Formal Scoreboard
8. Scale ItScaling the Tracker to a Packet RouterL3 Senior

   How does the same idea scale to a two-by-two packet router with several flows?

   Reveal the Model Answer

   Track one symbolic packet, tagged at the moment of acceptance. Count how many packets of its flow are owed ahead of it at its output. Assert that it leaves at its turn, on the right port, unchanged. Also assert that no output delivers a packet it does not owe. Fairness is a separate question: a fixed-priority arbiter passes every one of these safety checks.

   Read the diagram as text

   • input 0: tvalid, tdata, tdest
   • input 1: tvalid, tdata, tdest
   • grant per output: round-robin when both want it
   • queue 0: two entries {tid, tdata}
   • queue 1: two entries {tid, tdata}
   • output 0: tvalid, tdata, tid
   • output 1: tvalid, tdata, tid

   • input 0 → grant per output: 1 accepted
   • input 1 → grant per output
   • grant per output → queue 0: 2 queued
   • grant per output → queue 1
   • queue 0 → output 0: 3 its turn, 4 gone
   • queue 1 → output 1

   A two-by-two router with its tracked packet. tid names the input a packet came from.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Track one symbolic packet, tagged at the moment of acceptance. Key point 2 Count how many packets of its flow are owed ahead of it at its output. Key point 3 Assert that it leaves at its turn, on the right port, unchanged. Key point 4 Also assert that no output delivers a packet it does not owe. Key point 5 Fairness is a separate question: a fixed-priority arbiter passes every one of these safety checks.

   • Lesson F9.2Capstone: End-to-End Proof of a Packet Router
   • Problem F9.2.1Prove Packet Routing End to End
   • Problem F9.2.2Build the Router Packet Tracker
9. Prove ItSolve F9.2.1: Prove Packet Routing End to EndSimulator-graded

   Show it, don't just say it: this Silicon Lab problem is graded by the simulator.

   Open Problem F9.2.1