End-to-End Versus Glue Properties

Inside the Box, or Across It

A glue property, also called local or white-box, checks one piece of mechanism. An end-to-end property checks the block's purpose at its ports. Here that needs modelling code: a shadow copy of the contents, so the check knows which byte must come out next (F3.6).

A quick test: if the property names an internal signal, it is glue. If it names only ports and the bench's own model, it is end-to-end. Both kinds belong in a finished bench.

Each Kind Misses a Different Bug

The order bug leaves every pointer and count relation true; only the end-to-end check sees it. The count bug breaks the glue relation between count and the pointers one step after the cause, before any wrong byte reaches a port.

So end-to-end finds the bugs a user would see, and glue finds bugs earlier, closer to the cause. Glue properties also become the invariants that induction needs (F4.6).

End-to-End First, and What It Costs

Write end-to-end properties first: they restate the specification, and a sign-off argues about them (F7.3). Add glue second, to localise bugs and help proofs converge. A block with only glue properties is a block whose spec nobody wrote down.

The scoreboard is why the lab runs at depth 10: tracking data multiplies the work at every step.

Asked in Interviews

Try It

assert property (@(posedge clk) disable iff (rst) empty |-> wr_ptr == rd_ptr);
assert property (@(posedge clk) disable iff (rst) full |-> wr_ptr == rd_ptr);
assert property (@(posedge clk) disable iff (rst) count <= 3'd4);
assert property (@(posedge clk) disable iff (rst) count == f_ptr_diff || count == 3'd4 && f_ptr_diff == 2'd0);

assert property (@(posedge clk) disable iff (rst) pop && !empty |-> rdata == sb0);

[options]
mode bmc
depth 10
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv props.sv
prep -top fifo4sb
[files]
design.sv
props.sv

1. Run the glue set

   Run as it is, with the order bug: BMC PASS to depth 10.

2. Add the end-to-end check

   Append the end-to-end line to props.sv: FAIL at reported step 3. Compare rdata with sb0 at the pop.

3. Swap the bug

   Fix the read to mem[rd_ptr], then break the count update so a push and pop together count up. Run glue alone, then end-to-end alone.

4. Ask for depth 20

   On the correct design set depth 20. Expect the 20-second budget to end the run with no verdict; that result claims nothing.

Check Yourself

module fifo4sb(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr=0, rd_ptr=0;
  reg [2:0] count=0;
  assign full  = count == 3'd4;
  assign empty = count == 3'd0;
  wire wr_en = push && !full, rd_en = pop && !empty;
  assign rdata = mem[rd_ptr + 2'd1];   // bug: the pointer moves before the read
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      count <= count + wr_en - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire [1:0] f_ptr_diff = wr_ptr - rd_ptr;   // entries between the pointers, modulo 4
  // Modelling code: a shadow copy of the FIFO's contents, in order, oldest in sb0.
  reg [7:0] sb0=0, sb1=0, sb2=0, sb3=0;
  reg [2:0] sb_n=0;
  wire [2:0] slot = sb_n - (rd_en ? 3'd1 : 3'd0);   // where an accepted push lands
  always @(posedge clk)
    if (rst) sb_n <= 0;
    else begin
      if (rd_en) begin sb0 <= sb1; sb1 <= sb2; sb2 <= sb3; end
      if (wr_en) case (slot)
        3'd0: sb0 <= wdata;  3'd1: sb1 <= wdata;  3'd2: sb2 <= wdata;  default: sb3 <= wdata;
      endcase
      sb_n <= sb_n + wr_en - rd_en;
    end
`endif
endmodule

assert property (@(posedge clk) disable iff (rst) empty |-> wr_ptr == rd_ptr);
assert property (@(posedge clk) disable iff (rst) full |-> wr_ptr == rd_ptr);
assert property (@(posedge clk) disable iff (rst) count <= 3'd4);
assert property (@(posedge clk) disable iff (rst) count == f_ptr_diff || count == 3'd4 && f_ptr_diff == 2'd0);