Formal Interviews and Formal Careers

The Questions, by Level

Entry questions check the vocabulary of results: PASS at depth 20 is no failure in 20 steps, not a proof (F1.5). Mid questions check that you have fought a proof: what UNKNOWN means and what you add (F2.4). Senior questions check that you can say what a proof covers and sign it (F7.3).

The Loop, Stage by Stage

The trace stage decides most loops. You get a waveform and two minutes. Say the step, the cause and the fix, in that order, and say which of the four causes you ruled out.

In the bench-design stage the interviewer describes a block and asks what you would assume, assert and cover. Start from the spec rows, and name who checks each assumption.

Half an Answer, and a Whole One

Q: My assertion passed in simulation and
   failed in formal. Why?
A: The simulation did not have the right test.

A: Formal drives every input freely. Either
   the tests never reached the antecedent (a
   vacuous pass), or the solver found an input
   no legal driver makes: then I add an assumption.

The whole answer names both causes and the next step, so the follow-up is one the candidate wants (F1.2, F3.3).

What Postings Ask For

Formal roles sit mostly in CPU, GPU, networking and IP teams, and at a few formal consultancies. They are not a way around DV: the bench, the spec and the trace come first. This page prints no salary or demand figure: none we could trace to a named, dated source.

Getting started looks the same everywhere: pick a block, run covers before any assert, and show a designer a trace on their own RTL. A first result a designer can read builds more trust than any tool demo.

The Drill: Five Traces

For each trace, name the cause (RTL, assumption, property or reset) and the step, in under two minutes. Then write five properties from one-line specs and check them against the model answers; your spelling may differ.

Asked in Interviews

Try It

The lab is the drill. Each run reproduces one trace from its own lesson; read it before you look at the key.

1. Traces

   Run A to E. For each, write the cause and the failing sample before the timer reaches two minutes.

2. Properties

   FIFO: the next read returns the oldest write. Arbiter: a held request is granted within four cycles. Handshake: VALID holds until READY. W1C: a 1 clears, a 0 keeps. Timer: no bark without a full count.

3. Out loud

   Answer five entry questions from the wheel in one minute each, then compare with the lessons the rows name.

Check Yourself

module hs_ctrl(input clk, rst, req, abort, output reg ack);
  reg pending;
  reg pending_d;
  reg [1:0] busy_cnt;
  always @(posedge clk) begin
    if (rst) begin pending<=0; pending_d<=0; busy_cnt<=0; ack<=0; end
    else begin
      pending_d <= pending;
      if (abort) pending <= 0;
      else if (req) pending <= 1;
      else if (busy_cnt == 2'd3) pending <= 0;
      busy_cnt <= pending ? busy_cnt + 2'd1 : 2'd0;
      ack <= pending && busy_cnt == 2'd3;
    end
  end
  reg pending_q;
  always @(posedge clk) begin
    pending_q <= pending;
    if (!rst && ack) assert(pending_q);
  end
endmodule