The Sign-Off Argument

A Bounded PASS Needs a Second Number

A bounded PASS means nothing on its own. It becomes an argument next to the required depth: the shortest trace from reset that could show a violation. Reached above required is a bounded sign-off. Reached below it is a PASS and nothing more.

The Required-Depth Worksheet

Three lines carry the design: the deepest counter the property depends on, the longest transaction, and the property's own window (A2.1). The rest is bookkeeping. The engine agreed with the worksheet to the step.

Same Depth, Two Verdicts

When prove closes, the depth argument is unnecessary: the proof holds for all time. When it does not close, the report says "bounded, depth D, required R". A report that says only PASS has left the argument out.

k-induction at depth 12 returns UNKNOWN on the buggy block: no proof and no failure. PDR finds the counterexample, and on the fixed block it closes the proof, which needs no worksheet at all.

The Hidden Over-Constraint

assume property (@(posedge clk) pending && cnt >= 3 |-> grant_in);
cover property (@(posedge clk) !rst && pending && cnt == TMO - 1 && !grant_in);

cover property (@(posedge clk) !rst && pending && cnt == TMO - 1 && !grant_in);

One innocent-looking assumption made the timeout unreachable, and the proof of a buggy block passed. The cover caught it. Every assumption in a sign-off needs a reason from the spec and a cover that stays reachable under it.

The Four Cs

Each card is a list a reviewer can check line by line. Constraints come first, because one bad assumption voids every result after it, as the grant assumption just showed.

Required depth is the floor. A common margin is twice the deepest cover, so that two operations back to back fit inside the bound.

Asked in Interviews

Try It

The lab is tmo_blk with TMO = 6 and the late-error bug, bmc at depth 12: FAIL at reported step 10 in 0.5 s. The rule in concurrent SVA; the design runs it as req_q and an immediate assertion.

assert property (@(posedge clk) disable iff (rst) req && !pending |=> pending);

1. Fill the worksheet first

   Before running, compute the required depth for TMO = 6 and TMO = 12. Then run and compare the failing step.

2. Accept or reject?

   Set localparam TMO = 12; and run at depth 12. Write the sign-off line for that PASS, then rerun at the depth your worksheet asks for.

3. Find the over-constraint

   Add the assumption that the grant comes within four cycles, switch to abc pdr, then turn the check into the timeout cover. Read both.

Check Yourself

module tmo_blk(input clk, rst, req, grant_in, output reg pending = 0, output reg err = 0);
  localparam TMO = 12;
  reg [3:0] cnt = 0;      // waiting cycles
  reg late = 0;           // the cycle after a timeout
  always @(posedge clk)
    if (rst) begin pending <= 0; cnt <= 0; err <= 0; late <= 0; end
    else begin
      err <= late;
      late <= 0;
      if (!pending) begin
        if (req && !late) begin pending <= 1; cnt <= 0; end   // bug: a req in the late cycle is dropped
      end else if (grant_in) pending <= 0;
      else if (cnt == TMO - 1) begin pending <= 0; late <= 1; end
      else cnt <= cnt + 4'd1;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg req_q = 0;           // registered copy: a request seen while idle
  always @(posedge clk) begin
    req_q <= !rst && req && !pending;
    if (!rst && req_q) assert(pending);
  end
`endif
endmodule

module tmo_blk(input clk, rst, req, grant_in, output reg pending = 0, output reg err = 0);
  localparam TMO = 6;
  reg [3:0] cnt = 0;      // waiting cycles
  reg late = 0;           // the cycle after a timeout
  always @(posedge clk)
    if (rst) begin pending <= 0; cnt <= 0; err <= 0; late <= 0; end
    else begin
      err <= late;
      late <= 0;
      if (!pending) begin
        if (req && !late) begin pending <= 1; cnt <= 0; end   // bug: a req in the late cycle is dropped
      end else if (grant_in) pending <= 0;
      else if (cnt == TMO - 1) begin pending <= 0; late <= 1; end
      else cnt <= cnt + 4'd1;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg req_q = 0;           // registered copy: a request seen while idle
  always @(posedge clk) begin
    req_q <= !rst && req && !pending;
    if (!rst && req_q) assert(pending);
  end
`endif
endmodule