← Formal Verification Interviews
Interview Question · Concept
Using Formal to Close Coverage Holes
The Question
The interviewer asks
Simulation never hits three coverage bins. Can formal let you waive them, and what evidence would you accept?
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
Formal can ask three things of a bin: is it reachable, proven unreachable forever, or merely unreached within N steps. Only the proof supports a waiver; a bounded unreached cover is a hint about depth. In the lesson one bin is unreached at depth 20 and reached at step 26 at depth 30. Run the proof with as few assumptions as possible, since an over-constraint makes a live bin look dead.
Read the diagram as text
- A coverage bin: a Boolean condition on the design
- cover(bin), reached: reachable: here is the trace, a directed test
- assert(!bin), Prove PASS: unreachable from reset, for ever, under these assumptions
- cover(bin), unreached at N: not within N steps: a hint about depth
- Waive with the proof attached: mode, engine, assumptions, revision
- Raise N or try a proof: never a waiver by itself
- A coverage bin → cover(bin), reached
- A coverage bin → assert(!bin), Prove PASS
- A coverage bin → cover(bin), unreached at N
- assert(!bin), Prove PASS → Waive with the proof attached
- cover(bin), unreached at N → Raise N or try a proof
Reachable, proven unreachable and not reached within a bound are three different answers. Only the second one supports a waiver.
Measured with smtbmc yices, mode cover, depth 30. The last steps shown; steps 1 to 24 are all idle. A depth-20 run cannot hold this trace.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer separates three results: reachable, proven unreachable, and not reached within a bound.
What Interviewers Listen For (Senior)
A good senior answer writes waivers that carry the proof, its assumptions and the RTL revision. It hands reachable bins back to simulation as directed tests built from the cover traces.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompare
- Using Formal to Close Coverage Holes
-
WhyWhy Unreachability Runs Use Few AssumptionsL2 Mid-Level
Why should an unreachability run use as few assumptions as possible?
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
Free inputs allow more behaviour than the real environment. So a bin that cannot be reached even with free inputs cannot be reached in the chip. Every assumption you add shrinks the search and can make a live bin look dead. Add an assumption only when a reached trace is clearly illegal, and list it on the waiver.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F5.7.1: Prove the Dead Bins and Reach the Live OneSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfTurning a Cover Trace into a TestL2 Mid-LevelL3 Senior
Formal reaches a bin simulation never hit. What can you do with that trace?
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
Replay it as a directed test. SBY writes a small Verilog testbench for every trace. You can port the input values into the simulation environment as a sequence. The simulation team then has a test that hits the bin and keeps hitting it in regression. Every checker and scoreboard watches that test.
A Cover Trace Is a Directed TestYou name the state; the solver writes the stimulus. SBY saves the trace as a waveform and as a testbench that replays it. Arrows mean "becomes". Read the diagram as text
- cover(full): the state you want to see
- trace.vcd: every signal, step by step
- trace_tb.v: the same inputs as a Verilog testbench
- Any simulator: replays the inputs on the same RTL
- The same waveform: count climbs to 16, full rises
- cover(full) → trace.vcd: solver
- cover(full) → trace_tb.v: solver
- trace_tb.v → Any simulator
- Any simulator → The same waveform
The cheapest directed test there is: one line of SVA, no sequence to write.
Self-Check
Tick each key point you covered in your answer.
-
CompareFull Formal vs Semiformal SearchL2 Mid-LevelL3 Senior
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.
-
CompareA Formal Cover vs a Covergroup BinL1 JuniorL2 Mid-Level
How does a formal
coverdiffer from a covergroup bin that simulation hits?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 covergroup bin counts what your tests happened to do. A formal cover asks whether any legal input sequence can reach the condition and returns the shortest trace that does. An unreached formal cover within a bound only says the depth was too short or an assumption blocks it. A proof of the negation is what makes a bin truly unreachable.
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
"The cover came back unreached, so the bin is dead code."
Unreached within the bound is not a proof. The bin here is unreached at depth 20 and reached at step 26 once the depth is 30.
Run It
A coverage bin written as a cover on the idle timer, run at depth 20.
module seq25(input clk, rst, busy, start, output expired, output reg [1:0] phase=0);
reg [4:0] idle_cnt=0;
assign expired = idle_cnt == 5'd24;
always @(posedge clk) begin
if (rst) begin idle_cnt<=0; phase<=0; end
else begin
if (busy) idle_cnt <= 0;
else if (expired) idle_cnt <= 0;
else idle_cnt <= idle_cnt + 5'd1;
if (expired) phase <= 2'd0;
else if (start) phase <= phase + 2'd1;
end
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
bin_b: cover(idle_cnt == 5'd24 && start);
end
`endif
endmodule
Prints: cover, depth 20 (smtbmc yices): FAIL, cover unreached
See the Fix
module seq25(input clk, rst, busy, start, output expired, output reg [1:0] phase=0);
reg [4:0] idle_cnt=0;
assign expired = idle_cnt == 5'd24;
always @(posedge clk) begin
if (rst) begin idle_cnt<=0; phase<=0; end
else begin
if (busy) idle_cnt <= 0;
else if (expired) idle_cnt <= 0;
else idle_cnt <= idle_cnt + 5'd1;
if (expired) phase <= 2'd0;
else if (start) phase <= phase + 2'd1;
end
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
bin_b: cover(idle_cnt == 5'd24 && start);
end
`endif
endmodule
Prints: cover, depth 30 (smtbmc yices): PASS at step 26, cover reached
Missed Corner
"Waive it; the tool said unreachable."
A waiver needs the bin, the proof, the assumptions used and the RTL revision. Without the assumptions nobody can tell a dead bin from an over-constrained one.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 7 "Unreachable coverage elimination"