← Formal Verification Interviews
Interview Question · Code Writing
Writing a First Formal Testbench
- Likely at Apple
- Likely at MediaTek
- Likely at Siemens EDA
The Question
The interviewer asks
Write the formal bench for a one-entry register slice with valid/ready on both sides. What goes in it, and what is missing compared with a simulation testbench?
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
A formal bench has four parts: the DUT, assumptions on inputs, assertions on outputs and state, and covers. There is no driver, clock generator or scoreboard class, because the solver chooses every input. For the slice, assume upstream holds in_valid and its data until accepted. Assert the same rule on the output side. Cover a stall and a back-to-back transfer.
Read the diagram as text
- Solver: any value on every input, every step (F1.2)
- Assumptions: about inputs: what the neighbours promise
- slice (the DUT): the synthesised RTL, untouched
- Bound checker: ports and internals as inputs, compiled only for the formal run
- Assertions: about outputs and state: what the DUT promises
- Covers: what must stay possible (F3.5)
- Solver → slice (the DUT): in_valid, in_data, out_ready
- Assumptions → Solver: prunes
- slice (the DUT) → Bound checker: bind
- Bound checker → Assumptions: in
- Bound checker → Assertions: out
- Bound checker → Covers
No driver, no clock generator, no scoreboard class. The checker is the only monitor, and every rule in it is either a promise about an input or a claim about an output.
Measured with smtbmc yices at depth 20. The stall starts at step 2; the sampled violation is step 3, reported at step 4. The byte values are the solver's choice.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Fresher)
A good fresher answer lists the four parts and says the solver is the stimulus. It puts assumptions on inputs and assertions on outputs.
What Interviewers Listen For (Mid-Level)
A good mid-level answer adds data-integrity checks. It keeps registered copies where the engine cannot use the history of an input. It runs covers before it trusts any assertion.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompare
- Writing a First Formal Testbench
-
WhyWhy a Formal Bench Needs No StimulusL0 FresherL1 Junior
Why does a formal bench need no stimulus, and what takes the place of a coverage model?
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 solver treats every input as free and considers all legal values on every cycle. So writing stimulus would only narrow the search. Assumptions say what is legal. Covers replace the coverage model. Each one asks whether a behaviour is reachable under those assumptions, and returns a trace if it is.
Self-Check
Tick each key point you covered in your answer.
-
What IfA Formal Bench with No AssumptionsL1 Junior
What if you run the bench with no assumptions at all? What do you expect to see first?
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
Expect failures that no real neighbour could cause, because every input is free on every cycle. For example, the data changes while
validwaits forready. Triage each one: check the reset state, then each input against the spec. Add one assumption per spec rule, and cover the behaviour you still expect.Self-Check
Tick each key point you covered in your answer.
Misconception
"A failure with free inputs is always an RTL bug."
Free inputs can send sequences the protocol forbids. Check every shaded input against the spec before you touch the RTL.
Source Lesson F3.3 key points; Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 4 "Creating assumptions", Tip 4.3
-
Prove ItSolve F3.1.1: Build the Register-Slice CheckerSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfChecking a Transformed PayloadL1 JuniorL2 Mid-Level
What if the slice adds one to the payload instead of passing it through? How does the check change?
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
Capture the accepted input in modelling code. When the word leaves, assert that the output equals the same function of it, here the captured value plus one. The modelling code only reads design signals; it never drives them.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F3.1.2: Check the Transformed PayloadSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Break ItReusing a Protocol Checker on the Other SideL2 Mid-LevelL3 Senior
You have an APB property file written for the completer. How do you reuse it to verify the requester?
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
Write each rule once with its owner, and let a parameter choose assume or assert. Rules owned by the side under test are asserted, and the rest are assumed. A rule that flips from assertion to assumption is no longer checked on the new bench. So review it and cover what it might exclude. Watch for over-strict rules, such as forbidding PREADY high while PENABLE is low, which APB allows.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F8.5.1: One APB Contract on Both SidesSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareConcurrent Property vs Clocked Immediate FormL1 JuniorL2 Mid-Level
Compare the two ways of writing the output stall rule below: a concurrent property, and a clocked immediate assertion over registered copies.
systemverilog // concurrent form assert property (@(posedge clk) disable iff (rst) out_valid && !out_ready |=> out_valid && $stable(out_data)); // clocked immediate form always @(posedge clk) begin out_stall_q <= !rst && out_valid && !out_ready; out_data_q <= out_data; if (!rst && out_stall_q) assert(out_valid && out_data == out_data_q); end2: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
They check the same rule. The
|=>is one flop of delay, and$stablecompares with last cycle's sample. So the immediate form registers the stall condition and the data, and asserts on them a cycle later. In the lesson both forms fail the buggy slice at step 4. The immediate form helps where an engine refuses history functions on primary inputs, as this one does.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
Writes the output-side stall rule as an assume "so both sides match".
An assumption on the output deletes the failing traces. The slice that reloads data during a stall then passes; written as an assertion, the rule fails at step 4.
Run It
The register slice from lesson F3.1, which loads data during a stall, with the output rule assumed.
module slice(input clk, rst, in_valid, input [7:0] in_data, input out_ready,
output in_ready, output reg out_valid=0, output reg [7:0] out_data=0);
assign in_ready = !out_valid || out_ready;
always @(posedge clk) begin
if (rst) out_valid <= 0;
else if (in_ready) out_valid <= in_valid;
if (in_valid) out_data <= in_data; // bug: loads during a stall
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg [7:0] in_data_q=0; // last cycle's in_data
always @(posedge clk) in_data_q <= in_data;
reg in_stall_q=0, out_stall_q=0, accept_q=0;
reg [7:0] out_data_q=0;
always @(posedge clk) begin
in_stall_q <= !rst && in_valid && !in_ready;
out_stall_q <= !rst && out_valid && !out_ready;
accept_q <= !rst && in_valid && in_ready;
out_data_q <= out_data;
if (!rst && in_stall_q) assume(in_valid && in_data == in_data_q); // in: upstream
if (!rst && out_stall_q) assume(out_valid && out_data == out_data_q); // out: downstream
if (!rst && accept_q) assert(out_valid);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
See the Fix
module slice(input clk, rst, in_valid, input [7:0] in_data, input out_ready,
output in_ready, output reg out_valid=0, output reg [7:0] out_data=0);
assign in_ready = !out_valid || out_ready;
always @(posedge clk) begin
if (rst) out_valid <= 0;
else if (in_ready) out_valid <= in_valid;
if (in_valid) out_data <= in_data; // bug: loads during a stall
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg [7:0] in_data_q=0; // last cycle's in_data
always @(posedge clk) in_data_q <= in_data;
reg in_stall_q=0, out_stall_q=0, accept_q=0;
reg [7:0] out_data_q=0;
always @(posedge clk) begin
in_stall_q <= !rst && in_valid && !in_ready;
out_stall_q <= !rst && out_valid && !out_ready;
accept_q <= !rst && in_valid && in_ready;
out_data_q <= out_data;
if (!rst && in_stall_q) assume(in_valid && in_data == in_data_q); // in: upstream
if (!rst && out_stall_q) assert(out_valid && out_data == out_data_q); // out: downstream
if (!rst && accept_q) assert(out_valid);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 4
Misconception
"Reuse the simulation driver to generate stimulus for the formal run."
In formal the inputs are free and the solver drives them. A driver would pin one sequence and throw away the reason to use formal.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 4 "Bringing up a basic FPV environment"
Half-Truth
"Swap every assert and assume to reuse the checker on the other side."
A flipped assertion becomes an unchecked assumption on the new bench. Each one needs review and a cover of what it might exclude.