Formal for Post-Silicon Debug

The Symptom Is a Cover

Post-silicon formal turns the usual question around. The symptom (a register dump, two status bits, a stuck handshake) becomes a cover. What the lab observed becomes assume statements. The tool builds the shortest input sequence that matches.

On hs2 the cover is stuck = req_fsm == WAIT_GNT && arb_fsm == IDLE && !req_pending. Under the lab notes: Cover reached, reported step 6. The abort arrives in the one cycle when the request is pending, the arbiter has not sampled it, and its clock enable is low.

Which Observation Mattered

Assumptions can only remove traces, so the run without them is never longer: 5 against 6. The solver then gated the clock itself. Forcing the gating off makes the symptom unreachable: the clock gating was essential, which tells the lab where to look.

The assume(!abort) row is the trap. The lab did not see an abort because it did not look; assuming one away removes the cause, and the symptom looks impossible (F3.2).

A Hypothesis, Then a Proof

R_WAIT: if (gnt) req_fsm <= R_ACT;
// an abort before the sample clears
// req_pending, but WAIT_GNT ignores it

R_WAIT: if (gnt) req_fsm <= R_ACT;
  else if (abort && arb_fsm == A_IDLE)
    req_fsm <= R_IDLE;

A reached cover is one sequence that produces the symptom. The silicon may have failed another way, so replay the trace on the bench and prove the fix: the same assert, under the same environment, from reset.

This works only if the block's formal bench still exists when silicon returns, months after the RTL froze. Archive the bench, the suite version and the measured logs at tape-out.

Asked in Interviews

Try It

cover property (@(posedge clk) !rst && stuck);
assert property (@(posedge clk) disable iff (rst) !stuck);

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(*) begin assume(dma_en); assume(cg_en); end   // the lab notes
  always @(posedge clk) if (!rst) cover(stuck);

[options]
mode cover
depth 40
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top hs2
[files]
design.sv

1. Write the symptom

   The lab saw "waiting for grant" from the requester and "idle, nothing pending" from the arbiter. Write the cover from those bits.

2. Run under the lab notes

   Run as it is: Cover reached, reported step 6. Find the abort and the value of clk_en at that step.

3. Drop the notes

   Delete the assumptions: Cover reached, reported step 5. Then assume !cg_en: Cover unreached within 40. Which observation mattered?

4. Fix and prove

   Add the abort branch to WAIT_GNT, change the cover to assert(!stuck) and run abc pdr: Prove PASS (abc pdr).

Check Yourself

module hs2(input clk, rst, start, abort, dma_en, cg_en, output gnt, output stuck);
  localparam R_IDLE=2'd0, R_REQ=2'd1, R_WAIT=2'd2, R_ACT=2'd3;
  localparam A_IDLE=2'd0, A_SAMPLE=2'd1, A_GRANT=2'd2;
  reg [1:0] req_fsm=R_IDLE, arb_fsm=A_IDLE;
  reg req_pending=0, clk_en=1;
  wire req = req_fsm == R_REQ;
  assign gnt = clk_en && arb_fsm == A_GRANT;
  always @(posedge clk)
    if (rst) begin req_fsm <= R_IDLE; arb_fsm <= A_IDLE; req_pending <= 0; clk_en <= 1; end
    else begin
      clk_en <= cg_en ? !clk_en : 1'b1;            // clock gating: the arbiter steps every other cycle
      case (req_fsm)
        R_IDLE: if (start && dma_en) req_fsm <= R_REQ;
        R_REQ:  req_fsm <= abort ? R_IDLE : R_WAIT;
        R_WAIT: if (gnt) req_fsm <= R_ACT;
        R_ACT:  req_fsm <= R_IDLE;
      endcase
      if (abort && arb_fsm == A_IDLE) req_pending <= 0;   // abort before the sample cancels the request
      else if (req) req_pending <= 1;
      else if (gnt) req_pending <= 0;
      if (clk_en) case (arb_fsm)
        A_IDLE:   if (req_pending) arb_fsm <= A_SAMPLE;
        A_SAMPLE: arb_fsm <= A_GRANT;
        default:  arb_fsm <= A_IDLE;
      endcase
    end
  assign stuck = req_fsm == R_WAIT && arb_fsm == A_IDLE && !req_pending;
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(*) begin assume(dma_en); assume(cg_en); end   // the lab notes
  always @(posedge clk) if (!rst) cover(stuck);
`endif
endmodule