ASIC Point Explore

Cutpoints and Blackboxes

Free an internal signal to shrink the cone, see why that can only add failures, and tell a real counterexample from one the cut invented.

Lesson
F4.2
Time
20 min
Runs on
SymbiYosys
Check
5 questions

The packet buffer’s pointer proof ran out of time every night for a week. Its cone held a memory of sixteen 64-bit words and a CRC check, though the assertions only talked about pointers. One line, a free input in place of the CRC result, made it finish in 1.7 s.

A Cut Adds Behaviour

Three Places to Cut the Packet BufferThe assertions talk about pointers and the count. The memory and the CRC check reach them only through the drop decision; the full flag reaches them directly.
Three places to cut the packet bufferThe assertions talk about pointers and the count. The memory and the CRC check reach them only through the drop decision; the full flag reaches them directly. input wdata, wr 64-bit words: CRC inthe top 16 bits blackbox memory, 16 × 64 cut B: blackbox, everyoutput free cut CRC-16 check cut A: bad becomes afree input cut full flag cut C: control, givesa false failure control wr_ptr, rd_ptr,count a corrupt head wordis dropped property assertions empty |-> pointersequal; count <= 16 head worddropwrite enablecount == 16
Read the diagram as text
  • wdata, wr: 64-bit words: CRC in the top 16 bits
  • memory, 16 × 64: cut B: blackbox, every output free
  • CRC-16 check: cut A: bad becomes a free input
  • full flag: cut C: control, gives a false failure
  • wr_ptr, rd_ptr, count: a corrupt head word is dropped
  • assertions: empty |-> pointers equal; count <= 16
  • wdata, wr → memory, 16 × 64
  • memory, 16 × 64 → CRC-16 check: head word
  • CRC-16 check → wr_ptr, rd_ptr, count: drop
  • full flag → wr_ptr, rd_ptr, count: write enable
  • wr_ptr, rd_ptr, count → full flag: count == 16
  • wr_ptr, rd_ptr, count → assertions

Cuts A and B remove the datapath from the cone. Cut C removes a fact the assertions depend on.

A cut point replaces a signal with a free input, and the logic that drove it leaves the cone. The cut model can do everything the real design does, and more. So a PASS on the cut model holds for the real design; a FAIL may be one the real design cannot produce.

On the cut designPASSFAIL or reached
assertionholds for the real designtriage: could the real logic drive the cut signal that way?
coverunreached: unreachable in the real design tooreached: proves nothing if the trace uses the cut signal

A cut flips which results you can trust: for assertions, PASS; for covers, unreached.

A blackbox does the same to a whole module: every output becomes a cut point. Yosys has a cutpoint pass for both. The site’s runner fixes its own script, so the lab writes the free value into the RTL with $anyseq.

Cut the Datapath

Real CRC check

wire bad = crc16(head[47:0]) != head[63:48];

abc pdr: time limit (20 s), no verdict.

Cut point

wire bad = $anyseq;

abc pdr: Prove PASS, 1.7 s.

RunMeasured result
real design, abc pdr, the site’s runner (limit 20 s)time limit (20 s), no verdict
real design, abc pdr, SBY directly (limit 180 s)Prove PASS, 14.0 s
cut A: CRC result free, abc pdrProve PASS, 1.7 s
cut B: memory blackboxed, abc pdrProve PASS, 2.0 s
faulty read pointer, cut A, abc pdrFAIL at step 23, 0.9 s
faulty read pointer, real design, bmc 24FAIL at step 19, 2.9 s

The faulty twin wraps the read pointer at 16 while the write pointer wraps at 32. With the cut it still fails. Flop bits after prep: 15 real, 15 with cut A, 15 with cut B.

The pointers never care why a word is dropped, only that a drop moves rd_ptr like a read. Cutting bad keeps that and takes the CRC and the memory out of the cone, since nothing else reads the head word. The blackbox reaches the same cone from the other side.

Run the faulty twin after every cut. If it still fails, the cut kept the logic the bug lives in. If it passes, you cut too much, or the bug was in the logic you cut, and that logic needs its own proof.

Cut the Control: A False Failure

012345678910111213141516171819clkfreewrfreefullcount0123456789101112131415161716wr_ptr01234567891011121314151617rd_ptrcount 16, full 0count 17: violationreported

Measured counterexample with the full flag cut (bmc, depth 24): FAIL at step 19, 2.7 s. The free full is shaded like an input.

Cut the full flag instead and bmc fails at step 19. Step 17 shows count = 16 with full = 0, a pair the real flag never produces, and the write takes count to 17. The cut removed the very fact the assertion depends on.

Triage a cut-model failure like any counterexample: find the cut signal in the trace and ask whether the real logic could drive that value there. Here it could not. Do not undo the cut: constrain the free value with what the removed logic guaranteed, and prove that guarantee on the real logic.

RunMeasured result
cuts A and C plus assume(count != 16 || full), abc pdrProve PASS, 2.2 s
the guarantee asserted on the real flag, prove 2Prove PASS, 0.5 s
cuts A and C plus the assumption, faulty read pointer, bmc 24FAIL at step 19, 2.6 s
cover of count == 17, full cut, depth 24cover reached at step 19, 0.8 s
cover of count == 17, real design, depth 24cover unreached within depth 24, 0.8 s

The assumption states only what the real flag guarantees, and a separate run proves it. The reached cover on the cut design is the invented overflow.

This is assume-guarantee on a single wire (F4.3). The cover rows show the other half of the verdict table: the cut design reaches a count of 17, and the real one never does.

Asked in Interviews

QuestionAnswer
What is a cutpoint? Is it sound?An internal signal made a free input, so its fan-in leaves the cone. It is sound: the cut model has every real behaviour, so a PASS carries over. It can add false failures, never hide a real one.
What is blackboxing?Replacing a module by free outputs. Typical targets: memories, arithmetic, analog models, IP verified elsewhere. The logic inside is then not verified by this run.
How do you know a cut-model failure is real?Look at the cut signal in the trace. If the real logic could produce that value at that step, the failure is real; if not, refine the cut or add a proven assumption.

Try It

The lab is the buffer with the CRC result cut, prove with abc pdr. Measured: Prove PASS, 1.7 s. Without the cut: time limit (20 s), no verdict in the runner; Prove PASS, 14.0 s with SBY directly.

The two rules in concurrent SVA. The lab runs them as immediate assertions.
assert property (@(posedge clk) disable iff (rst) empty |-> wr_ptr == rd_ptr);
assert property (@(posedge clk) disable iff (rst) count <= 16);

  1. Move the cut

    Put the CRC check back and blackbox the memory instead: give pbuf_mem the single line assign rd = $anyseq;. Compare the time.

  2. Check soundness

    Make the read pointer wrap at 15 (rd_ptr == 5'd15 ? 5'd0 : rd_ptr + 5'd1) and run again with the cut.

  3. Cut the control

    Restore the design and cut full instead. Run bmc at depth 24 and find the step where count and full disagree.

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 buffer with its read pointer wrapping at 16, CRC result cut to $anyseq, mode prove, abc pdr, reset assumed in step 0. The verdict is:
      
module pbuf_mem(input clk, we, input [3:0] wa, ra, input [63:0] wd, output [63:0] rd);
  reg [63:0] m [0:15];
  always @(posedge clk) if (we) m[wa] <= wd;
  assign rd = m[ra];
endmodule
module pbuf(input clk, rst, wr, rd, input [63:0] wdata, output [63:0] rdata, output fwd, empty);
  reg [4:0] wr_ptr = 0, rd_ptr = 0, count = 0;
  wire full = count == 5'd16;
  assign empty = count == 5'd0;
  wire do_wr = wr && !full;
  wire [63:0] head;
  pbuf_mem u_mem(.clk(clk), .we(do_wr), .wa(wr_ptr[3:0]), .ra(rd_ptr[3:0]), .wd(wdata), .rd(head));
  function [15:0] crc16(input [47:0] d);   // CRC-16/CCITT over the payload
    integer i; reg [15:0] x;
    begin x = 16'hFFFF;
      for (i = 47; i >= 0; i = i - 1) x = {x[14:0], 1'b0} ^ ((x[15] ^ d[i]) ? 16'h1021 : 16'h0000);
      crc16 = x;
    end
  endfunction
  wire bad = $anyseq;                // cut point on the datapath
  assign rdata = head;
  assign fwd = !empty && !bad;
  wire do_rd = !empty && (bad || rd);    // a corrupt head word is dropped
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (do_wr) wr_ptr <= wr_ptr + 5'd1;
      if (do_rd) rd_ptr <= rd_ptr == 5'd15 ? 5'd0 : rd_ptr + 5'd1;   // bug: wraps at 16
      count <= count + do_wr - do_rd;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);
    assert(count <= 5'd16);
  end
endmodule


      

      

      


Predict the outputThe correct buffer with full cut to $anyseq, mode bmc, depth 24, smtbmc yices, reset assumed in step 0. At which step does SBY report the failure?
      
module pbuf_mem(input clk, we, input [3:0] wa, ra, input [63:0] wd, output [63:0] rd);
  reg [63:0] m [0:15];
  always @(posedge clk) if (we) m[wa] <= wd;
  assign rd = m[ra];
endmodule
module pbuf(input clk, rst, wr, rd, input [63:0] wdata, output [63:0] rdata, output fwd, empty);
  reg [4:0] wr_ptr = 0, rd_ptr = 0, count = 0;
  wire full = $anyseq;               // cut point on a control signal
  assign empty = count == 5'd0;
  wire do_wr = wr && !full;
  wire [63:0] head;
  pbuf_mem u_mem(.clk(clk), .we(do_wr), .wa(wr_ptr[3:0]), .ra(rd_ptr[3:0]), .wd(wdata), .rd(head));
  function [15:0] crc16(input [47:0] d);   // CRC-16/CCITT over the payload
    integer i; reg [15:0] x;
    begin x = 16'hFFFF;
      for (i = 47; i >= 0; i = i - 1) x = {x[14:0], 1'b0} ^ ((x[15] ^ d[i]) ? 16'h1021 : 16'h0000);
      crc16 = x;
    end
  endfunction
  wire bad = crc16(head[47:0]) != head[63:48];
  assign rdata = head;
  assign fwd = !empty && !bad;
  wire do_rd = !empty && (bad || rd);    // a corrupt head word is dropped
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (do_wr) wr_ptr <= wr_ptr + 5'd1;
      if (do_rd) rd_ptr <= rd_ptr + 5'd1;
      count <= count + do_wr - do_rd;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);
    assert(count <= 5'd16);
  end
endmodule


      

      

      


ConceptWhich statement about a cut point is wrong?


ConceptWhy did cutting the CRC result also remove the memory from the cone?


Read the waveformWhich pair of values in this trace can the real design never have?

    
  012345678910111213141516171819clkfreewrfreefullcount0123456789101112131415161716wr_ptr01234567891011121314151617rd_ptrcount 16, full 0count 17: violationreported
Measured counterexample with the full flag cut (bmc, depth 24): FAIL at step 19, 2.7 s. The free full is shaded like an input.

        

        
      

    

    
Remember
  • A cut point or blackbox frees signals and shrinks the cone; it over-approximates the design.
  • PASS on the cut model is a real PASS; FAIL must be checked at the cut signal.
  • Cut datapath that the property does not read; never cut the control it depends on.
  • Run the faulty twin after every cut.