← Formal Verification Interviews
Interview Question · Design
Assume-Guarantee Without Circular Logic
- Likely at MediaTek
- Likely at Arm
The Question
The interviewer asks
Two blocks are too big to prove together, so you prove each one assuming the other behaves. When is that sound, and when does it prove a bug away?
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
Prove each block's guarantee while assuming the other's, then compose. For safety this is sound when each assumption is only needed for earlier cycles, not the current one. If each block assumes the other's guarantee in the same cycle, the proofs lean on each other. Both can then pass with a real bug. In the lesson's credit link the circular version passes; assuming only last cycle's guarantees finds the bug.
Read the diagram as text
- snd: two credits; sends only with a credit
- rcv: two buffer slots; registered credit return
- G_A: no send while two words are outstanding
- G_B: no credit while nothing is outstanding
- out_cnt: interface monitor: sends minus credits
- snd → rcv: send
- rcv → snd: ret
- G_A → rcv: assumed by
- G_B → snd: assumed by
- out_cnt → G_A
- out_cnt → G_B
G_A is proved on snd under G_B; G_B is proved on rcv under G_A.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Senior)
A good senior answer states the earlier-cycle condition, and shows how same-cycle assumptions mask a bug. It checks that every interface assumption is asserted on the block that owns it.
What Interviewers Listen For (Staff)
A good staff answer uses contracts to plan a subsystem proof: one per boundary, each proven on its owner. It joins them with the time-shift rule, and reviews the contracts like a spec.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyProve ItBreak ItCompareScale It
- Assume-Guarantee Without Circular Logic
-
WhyWhy Last Cycle's Guarantee Is EnoughL3 Senior
Why does assuming only the other block's guarantee from the previous cycle make the argument sound?
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
It turns the pair of proofs into induction over time. At reset both guarantees hold. Suppose both held up to cycle t minus one. Then each block's proof shows its own guarantee at cycle t, so both hold at t. A same-cycle assumption breaks that chain, because each guarantee at t would rest on the other at t.
Self-Check
Tick each key point you covered in your answer.
-
Break ItTwo Wrong Blocks That Both ProveL3 Senior
Break it: show how two same-cycle assumptions can let two wrong blocks both prove.
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
Block A assumes B sends good data this cycle, and B assumes the same of A. Suppose both send bad data in the same cycle. Each proof rules that case out by its own assumption, so both pass. The time shift breaks the circle, because cycle t then rests only on cycle t minus one.
Self-Check
Tick each key point you covered in your answer.
Misconception
"Each block is proven, so the pair is proven."
Each proof assumed the other block correct in the same cycle. Together they assume what they set out to prove, so a joint failure goes unseen.
Source Lesson F4.3 key points
-
Prove ItSolve F4.3.2: Break the Circular GuaranteeSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareCase Splitting a Hard ProofL2 Mid-LevelL3 Senior
What if a property is hard only for some opcodes or address ranges? How do you split it safely?
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
Run the proof once per case, each with an assumption that pins the case variable. Prove separately that the cases together cover every value. Pin the case for the whole run, from a value fixed at the start. A split that lets the case change each cycle can hide interleavings between cases. The slow case then shows you where the hard logic is.
One Proof Becomes ThreeThe assertion is proved once per burst type. The three cases together are every legal burst, because the request never carries burst type 3. Read the diagram as text
- every legal burst: FIXED, INCR or WRAP, any order
- case FIXED: busy && burst_q == FIXED |-> in page
- case INCR: busy && burst_q == INCR |-> in page
- case WRAP: busy && burst_q == WRAP |-> in page
- union: the three conditions cover every busy cycle
- every legal burst → case FIXED
- every legal burst → case INCR
- every legal burst → case WRAP
- case FIXED → union
- case INCR → union
- case WRAP → union
Soft split: the case is the assertion’s condition, so each run still allows any sequence of bursts.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F4.3.1: An Exhaustive Address Case SplitSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Scale ItContracts for a Six-Block SubsystemL4 Staff
How would you use interface contracts to verify a subsystem of six blocks formally?
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 one contract per boundary from the interface spec. Prove each block against the contracts of its neighbours, assumed with the time-shift rule. Each contract is asserted on its owner and bound into system simulation as a check. The end-to-end goals that cross several blocks then rest on proven contracts, and a contract change triggers a review of both sides.
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
"If each block passes while assuming the other, the pair is proven."
Here the receiver pops an empty buffer. Both guarantees are assumed in the same cycle as they are asserted, so the run passes. Assuming only the previous cycle's guarantees fails at step 3.
Run It
A two-credit link from lesson F4.3: sender and receiver guarantees assumed in the same cycle they are checked.
module snd(input clk, rst, want, ret, output send);
reg [1:0] cred = 2'd2;
assign send = want && cred != 2'd0;
always @(posedge clk) if (rst) cred <= 2'd2; else cred <= cred - send + ret;
endmodule
module rcv(input clk, rst, send, drain, output reg ret = 0);
reg [1:0] fill = 2'd0;
wire pop = drain; // bug: pops an empty buffer
always @(posedge clk)
if (rst) begin fill <= 0; ret <= 0; end
else begin fill <= fill + send - pop; ret <= pop; end
endmodule
module link(input clk, rst, want, drain);
wire send, ret;
snd a(.clk(clk), .rst(rst), .want(want), .ret(ret), .send(send));
rcv b(.clk(clk), .rst(rst), .send(send), .drain(drain), .ret(ret));
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg [2:0] out_cnt = 3'd0; // words sent minus credits returned
reg ok_q = 1'b1;
always @(posedge clk) begin
out_cnt <= rst ? 3'd0 : out_cnt + send - ret;
ok_q <= rst || (!(send && out_cnt == 3'd2) && !(ret && out_cnt == 3'd0));
end
always @(posedge clk) if (!rst) begin
assume(!(send && out_cnt == 3'd2));
assume(!(ret && out_cnt == 3'd0));
assert(!(send && out_cnt == 3'd2));
assert(!(ret && out_cnt == 3'd0));
end
endmodule
Prints: prove, depth 4 (abc pdr): PASS
See the Fix
module snd(input clk, rst, want, ret, output send);
reg [1:0] cred = 2'd2;
assign send = want && cred != 2'd0;
always @(posedge clk) if (rst) cred <= 2'd2; else cred <= cred - send + ret;
endmodule
module rcv(input clk, rst, send, drain, output reg ret = 0);
reg [1:0] fill = 2'd0;
wire pop = drain; // bug: pops an empty buffer
always @(posedge clk)
if (rst) begin fill <= 0; ret <= 0; end
else begin fill <= fill + send - pop; ret <= pop; end
endmodule
module link(input clk, rst, want, drain);
wire send, ret;
snd a(.clk(clk), .rst(rst), .want(want), .ret(ret), .send(send));
rcv b(.clk(clk), .rst(rst), .send(send), .drain(drain), .ret(ret));
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg [2:0] out_cnt = 3'd0; // words sent minus credits returned
reg ok_q = 1'b1;
always @(posedge clk) begin
out_cnt <= rst ? 3'd0 : out_cnt + send - ret;
ok_q <= rst || (!(send && out_cnt == 3'd2) && !(ret && out_cnt == 3'd0));
end
always @(posedge clk) if (!rst) begin
assume(ok_q); // both held in the previous cycle
assert(!(send && out_cnt == 3'd2));
assert(!(ret && out_cnt == 3'd0));
end
endmodule
Prints: prove, depth 4 (abc pdr): FAIL at step 3
Missed Corner
"Contracts only need checking where they are assumed."
A contract assumed on one block must be asserted and proven on the block that owns it, or nothing ever checks it.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 10 "Choosing the right battle"