Interview Question · Design

The Formal Sign-Off Argument

L3 SeniorL4 Staffsignoffmethodology

Likely at AMD
Likely at Qualcomm
Likely at Intel

The interviewer asks

You are asked to sign off a timeout block with formal. What has to be on the page before you put your name to it?

Reveal the Model Answer

Each of four items needs evidence. Every assumption has a spec reason and a cover reachable under it. The properties map to spec rows, and a mutation sample shows they notice faults. Each result is a full proof, or a bounded pass next to the depth the counters and transactions require. A cone map names the logic no property reads, and every line carries the tool version and date.

The Four Lists a Lead ReviewsConstraints, checkers, complexity and coverage: each list has an open-tool result under it.

Read the diagram as text

Constraints: every assumption, its reason, and a cover reached under it
Checkers: the spec checklist and a mutation score with its sample (F7.2)
Complexity: per property: full proof, or bounded with its worksheet; each abstraction with its soundness note
Coverage: the cone map, white logic named (F7.1); cover depths
One-page sign-off: the four lists, the depth bar per property, suite version, date

Constraints → One-page sign-off
Checkers → One-page sign-off
Complexity → One-page sign-off
Coverage → One-page sign-off

A gap in any list is a reason to reject, however green the runs are.

Cover depths against the bounded run

Four covers on the spine, reached at reported steps 3, 6, 6, 8. A bounded run must reach past the deepest one.

Linear scale. 0 to 20 steps.

Checked bound: 10
Required bound: 9
Claim: Bounded check only

Measured: one entry at step 3; full at step 6; full, push and pop together at step 6; full again after two reads at step 8. The spine passes bmc at depth 10.

Self-Check

Tick each key point you covered in your answer.

Key point 1 Each of four items needs evidence. Key point 2 Every assumption has a spec reason and a cover reachable under it. Key point 3 The properties map to spec rows, and a mutation sample shows they notice faults. Key point 4 Each result is a full proof, or a bounded pass next to the depth the counters and transactions require. Key point 5 A cone map names the logic no property reads, and every line carries the tool version and date.

What Interviewers Listen For (Senior)

A good senior answer lists the assumptions with their covers, and the required depth or a full proof. It maps every property to the spec. It also shows coverage of the cone.

What People Get Wrong

Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.

Missed Corner

"BMC passed at depth 12, longer than any transaction, so we are done."

With a 12-cycle timeout this bug needs 16 steps; the depth sweep shows depth 16 passing and 17 failing. The required depth comes from the deepest counter in the cone.

Run It

The timeout block from lesson F7.3 with a 12-cycle timeout, run at depth 12.

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

Prints: bmc, depth 12 (smtbmc yices): PASS

See the Fix

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

Prints: bmc, depth 20 (smtbmc yices): FAIL at step 16

Misconception

"PDR gave a full proof, so the assumptions do not matter."

Assuming the grant always comes within four cycles means the timeout can never fire. PDR proves the buggy block; a cover of the timeout path comes back unreached.

Run It

The same buggy block with "the grant comes within four cycles" assumed, proved by abc pdr.

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
  always @(*) if (pending && cnt >= 4'd3) assume(grant_in);   // the grant comes within four cycles
  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

Prints: prove, depth 20 (abc pdr): PASS

See the Fix

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
  always @(*) if (pending && cnt >= 4'd3) assume(grant_in);   // the grant comes within four cycles
  reg req_q = 0;           // registered copy: a request seen while idle
  always @(posedge clk) begin
    req_q <= !rst && req && !pending;
    if (!rst) cover(pending && cnt == TMO - 1 && !grant_in);
  end
`endif
endmodule

Prints: cover, depth 20 (smtbmc yices): FAIL, cover unreached

Wrong Altitude

Answers with tool commands and run times instead of an argument.

The question is what evidence makes the claim believable. Engine names are the smallest part of a sign-off.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

The Formal Sign-Off Argument

Your Answer

Self-Check

What Interviewers Listen For (Senior)

What Interviewers Listen For (Staff)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It

The Question

Your Answer

Self-Check

What Interviewers Listen For (Senior)

What Interviewers Listen For (Staff)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It