End-to-End vs Glue Properties

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

WhyWhat IfProve ItBreak ItCompareScale It

1. End-to-End vs Glue Properties
2. WhyWhy Glue Properties Miss Data BugsL2 Mid-Level

   Why can every pointer and count property hold while the FIFO returns the wrong data?

   Reveal the Model Answer

   Glue properties check the mechanism: pointers stay consistent with the count and full and empty agree with them. A bug in what is read, such as the wrong slot or stale data, leaves all of that intact. Only a property that compares what leaves with what entered, the purpose of the block, can see it.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Glue properties check the mechanism: pointers stay consistent with the count and full and empty agree with them. Key point 2 A bug in what is read, such as the wrong slot or stale data, leaves all of that intact. Key point 3 Only a property that compares what leaves with what entered, the purpose of the block, can see it.

   • Lesson F3.4End-to-End Versus Glue Properties
3. Prove ItSolve F3.4.1: Prove the Data, Not Just the PointersSimulator-graded

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

   Open Problem F3.4.1

4. CompareThe Formal Scoreboard with One Symbolic WordL2 Mid-LevelL3 Senior

   Write a formal check of data integrity and order through a FIFO, without modelling the whole queue.

   Reveal the Model Answer

   Track one word whose value comes from $anyconst, so the solver picks it once, and let the cycle it enters be free. Count the words ahead of it, then assert that it is never dropped and that it leaves first in line, unchanged. The value and entry time are arbitrary. So a proof for this one word covers every word, as long as the design never inspects the data.

   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.

   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
   

   Prints: prove, depth 2 (smtbmc yices): PASS

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Track one word whose value comes from $anyconst, so the solver picks it once, and let the cycle it enters be free. Key point 2 Count the words ahead of it, then assert that it is never dropped and that it leaves first in line, unchanged. Key point 3 The value and entry time are arbitrary. Key point 4 So a proof for this one word covers every word, as long as the design never inspects the data.

   What Interviewers Listen For (Mid-Level)

   A good mid-level answer describes the $anyconst value, the free entry time and the two assertions.

   Misconception

   "One tracked value proves the FIFO only for that value."

   The solver may choose any value and any entry time. If some word could be lost or reordered, the solver would pick that word, so the proof covers them all.

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

   Missed Corner

   "Shrink the data to one bit; a FIFO does not care about data."

   Only true when no logic reads the data. This FIFO drops a second 8'hFF in a row. The tracker finds it with the value 255, which a one-bit path could never carry.

   Run It

   A FIFO with fill-word compression: a repeated 8'hFF is not stored.

   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]];
     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 [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
   

   Prints: bmc, depth 12 (smtbmc yices): FAIL at step 4

   See the Fix

   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
   

   Prints: prove, depth 2 (smtbmc yices): PASS

   • Lesson F4.4Symbolic Constants and Data Independence: The Formal Scoreboard
   • Lesson F8.1A FIFO, End to End
   • Lesson F9.2Capstone: End-to-End Proof of a Packet Router
   • Problem F4.4.1Implement the Symbolic Packet Tracker
   • Problem F4.4.2Identity Before Payload Equality
5. 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
6. 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

7. 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
8. 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

9. 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
10. 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
11. 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
12. 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

13. Break ItWhat a Bounded End-to-End Check MissesL2 Mid-LevelL3 Senior

    Your end-to-end FIFO check passes at depth 10. What bug could still be there?

    Reveal the Model Answer

    Anything that needs more than ten steps to reach a port. Examples are a pointer that wraps wrongly only after many writes, or a count that drifts and overflows later. The end-to-end check sees the effect only once the bad word is read. Glue invariants on the count and pointers catch such drift early and also help an induction proof close.

    Correct FIFO, glue and end-to-end together. Depth 10 (samples 0 to 8) passed in 1.0 s. Depth 20 ended at the 20-second budget: time limit, no verdict.

    Linear scale. 0 to 20 steps.

    Checked bound

    10

    Required bound

    20

    Claim

    Bounded check only

    Glue and end-to-end checks together on a correct FIFO. Depth 10 passed in 1.0 s; depth 20 ran out of time.

    Self-Check

    Tick each key point you covered in your answer.

    Key point 1 Anything that needs more than ten steps to reach a port. Key point 2 Examples are a pointer that wraps wrongly only after many writes, or a count that drifts and overflows later. Key point 3 The end-to-end check sees the effect only once the bad word is read. Key point 4 Glue invariants on the count and pointers catch such drift early and also help an induction proof close.

    • Lesson F3.4End-to-End Versus Glue Properties
    • Lesson F8.1A FIFO, End to End