← Formal Verification Interviews
Interview Question · Concept
Formal Verification vs Simulation
- Asked at Qualcomm
- Likely at Infineon
- Likely at Micron
The Question
The interviewer asks
What is the difference between formal verification and simulation, and when would you pick each?
You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
Simulation checks the paths your stimulus happens to drive, so a rare corner is found only if some test reaches it. Formal treats the inputs as free. It asks a solver whether any input sequence breaks a property, within a bound or for all time. Pick formal for control logic with deep corners such as arbiters, FIFOs, protocol rules and registers. Keep simulation for long end-to-end flows, performance and whole-chip behaviour.
Ring k holds every state the arbiter can reach k cycles after reset, under every input sequence. The double grant sits in ring 4. A random run is one thread through these rings.
Four rings hold the double grant 011; a run to depth 20 covers twenty of them. The state 111 (three grants) is outside every ring: no input sequence produces it, so a cover on it would come back unreached.
Read the states and transitions
- gnt 000: initial, depth 0.
- gnt 010: reachable, depth 1.
- lock, 010: reachable, depth 2.
- reload 2: reachable, depth 3.
- gnt 011: bad, depth 4.
- gnt 111: unreachable, depth 0.
- gnt 000 → gnt 010.
- gnt 010 → lock, 010.
- lock, 010 → reload 2.
- reload 2 → gnt 011.
- gnt 010 → gnt 000.
- lock, 010 → gnt 010.
Illustration. A drawing of the idea, with the measured depth. The real arbiter has six flops and 64 possible states; only the ones on the counterexample are drawn.
Read the diagram as text
- Random simulation: paths; any design size; finds what the stimulus hits
- Formal property verification: states; bounded size; finds whatever is reachable
- Formal apps: narrow questions on large designs (F5)
- Equivalence checking: two designs, same outputs (F6)
- arb3 RTL: the same source for every tool
- arb3 RTL → Random simulation: one driven path
- arb3 RTL → Formal property verification: every input sequence
- Formal property verification → Formal apps: the same engines
- Formal property verification → Equivalence checking: the same solvers
Formal sits beside simulation, not in place of it. Both read the same RTL.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Fresher)
A good fresher answer says simulation checks only the paths a test drives, while formal checks every input sequence against a property. It names one block that suits each method.
What Interviewers Listen For (Senior)
A good senior answer adds that formal proves only the properties written, under the assumptions given. It splits a real block: formal for control corners, simulation for integration, performance and firmware flows.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompareScale It
- Formal Verification vs Simulation
-
WhyWhy Formal Finds What a Million Cycles MissL0 FresherL1 Junior
Why can a bug survive a million random cycles and then fall out of a formal run in seconds?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
A simulation is one path. A million cycles visit at most a million states, out of up to 2 to the power of the flop count. BMC at depth k reasons about every input sequence of length k from reset in one solver query. The solver picks the inputs that break the property, so a rare three-cycle pattern costs it nothing extra.
Self-Check
Tick each key point you covered in your answer.
-
What IfBlocks That Resist FormalL1 JuniorL2 Mid-Level
Which blocks are poor candidates for formal, and what do you do about them?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
Formal struggles when a property's cone is deep or hard: long counters, wide multipliers, big memories and whole-chip flows. A bounded run then stops short of the behaviour and a proof may never finish. One option is to change the question with cut points, abstraction and smaller parameters. The other is to leave that part to simulation and prove the control logic around it.
Self-Check
Tick each key point you covered in your answer.
-
WhyWhy a Wide Counter Defeats BMCL1 JuniorL2 Mid-Level
Why does a 16-bit timeout counter make a bounded proof hopeless, and what do you do instead?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
Reaching expiry from reset takes as many steps as the count. BMC must unroll every one of them, so the required depth runs into the tens of thousands. Instead, abstract the counter to the few values that matter and prove the abstraction on the real counter in a side run. A one-transition property can also be proven by induction at full width without ever reaching expiry.
Where the Bug Lives on the Real Timer, and Where Depth 40 StopsThe faulty watchdog's counterexample on the real timer: reset, start, 65,536 cycles of counting, then the kick that lands on the expiry. Depth 40 checks samples 0 to 38. Read the diagram as text
- step 0: reset: assumed
- step 1: start: pre and ticks captured, each at least 256
- steps 2 to 65,537: RUN: timer counts 0 to 65,535
- step 65,538: kick on expiry: the faulty FSM tests the expiry first
- step 65,539: bark: the violation; reported at step 65,540
- depth 40 ends at sample 38: required depth: 65,541
- step 0: reset → step 1: start
- step 1: start → steps 2 to 65,537
- steps 2 to 65,537 → step 65,538: kick on expiry
- step 65,538: kick on expiry → step 65,539: bark
- depth 40 ends at sample 38 → steps 2 to 65,537: stops inside the wait
Depth 40 covers 0.06 % of the bound the bug needs. The steps on the real timer follow from the measured cut trace plus 65,536 counting cycles.
Self-Check
Tick each key point you covered in your answer.
-
What IfIs the Abstract Counter SoundL2 Mid-LevelL3 Senior
You replace the 16-bit timeout counter with an abstract one that may expire at any time. Why is that sound, and what can it break?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
The abstract counter can do everything the real one does, plus more, such as expiring early. So a pass on the abstract model holds for the real design. The extra behaviour can cause false failures, for example an early timeout. Check each failure against the real counter, and prove the values you kept on the real design.
Self-Check
Tick each key point you covered in your answer.
Half-Truth
"The abstract model passes, so the real counter needs no checks."
The abstraction is sound only if it includes every real count sequence. Prove the values it keeps, such as reset and expiry, on the real counter.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 10 "Counter abstraction"
-
Prove ItSolve F1.2.1: Retire the Response, Including ErrorsSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Break ItA Proven Block with a Silicon BugL2 Mid-LevelL3 Senior
A block passed full formal proofs and still had a bug in silicon. How can that happen?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
The proof was true of what was written, not of what was meant. Common causes are a missing or weak property, or an assumption that removed legal inputs. Others are a bounded result read as a proof, or a bug outside every property's cone. The defences are a spec checklist, covers under the assumptions, a stated required depth and a cone map.
Self-Check
Tick each key point you covered in your answer.
-
Scale ItSplitting an IP Between Formal and SimulationL3 Senior
You own verification of a new IP. How do you decide what formal covers and what simulation covers?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
Split by question, not by team. Formal takes control logic whose rules fit in a few cycles: protocol compliance, arbitration, FIFO and credit invariants, registers, connectivity and deadlock. Simulation keeps data flows across many blocks, long scenarios, performance and firmware interaction. Every formal assumption is also bound into simulation as an assertion, so a wrong assumption is caught at system level.
Self-Check
Tick each key point you covered in your answer.
-
CompareFull Formal vs Semiformal SearchL2 Mid-LevelL3 Senior
Asked if they say formal cannot reach deep bugs
A refresh event happens only every few thousand cycles, far past any depth your proofs reach. Compare full formal with a semiformal search for bugs around that event.
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
Full formal searches every trace from reset, so a few thousand cycles of depth is out of reach. Semiformal starts the solver from a waypoint instead: a simulation or cover trace that has already run close to the event. It then searches exhaustively from there. It finds deep bugs that neither method finds alone. But it proves nothing about the states it skipped, so it counts as bug hunting, not sign-off.
Self-Check
Tick each key point you covered in your answer.
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"A million random cycles with no failure means the corner is covered."
The double grant in this arbiter needs a three-cycle pattern with per-cycle odds of 1/4096 × 1/256 × 1/512. Random stimulus rarely lines that up; BMC returns it at step 5.
Run It
The arbiter from lesson F1.1: a grant can double up only after weight A5 and the request sequence 110, 011, 111.
module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0);
reg lock=0;
reg [1:0] reload=0;
wire [2:0] pri = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000;
wire hold = lock && |(req & gnt);
always @(posedge clk) begin
if (rst) begin gnt<=0; lock<=0; reload<=0; end
else begin
lock <= weight[7];
reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0;
if (reload == 2'd2 && req == 3'b111) gnt <= gnt | pri; // reload cycle: lock holds, encoder grants too
else gnt <= hold ? gnt : pri;
end
end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
assert($onehot0(gnt));
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 5
See the Fix
module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0);
reg lock=0;
reg [1:0] reload=0;
wire [2:0] pri = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000;
wire hold = lock && |(req & gnt);
always @(posedge clk) begin
if (rst) begin gnt<=0; lock<=0; reload<=0; end
else begin
lock <= weight[7];
reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0;
if (reload == 2'd2 && req == 3'b111) gnt <= hold ? gnt : pri;
else gnt <= hold ? gnt : pri;
end
end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
assert($onehot0(gnt));
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
Half-Truth
"Once a block is formally proven you can drop its tests."
A proof covers the properties written, under the assumptions given, inside the block. Integration, performance and anything never written as a property still need simulation.
Buzzword Without Mechanism
Says "formal is exhaustive" and stops there.
Exhaustive over what? Over every input sequence the assumptions allow, up to the depth for a bounded run. Without the depth and the assumptions the word says nothing.