← Formal Verification Interviews
Interview Question · Code Writing
Formally Verifying a Round-Robin Arbiter
The Question
The interviewer asks
What properties would you write to verify a four-requester round-robin arbiter formally?
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
Start with one-cycle safety: at most one grant, and no grant without a request. Then pin the rotation: after granting requester i, the pointer moves just past i. Finally fairness: assuming requests hold until granted, every request is granted within a bounded number of cycles. Cover each requester being granted and a full round of grants.
Read the diagram as text
- ptr = 0: grant to 0 moves it to 1
- ptr = 1: grant to 1 moves it to 2
- ptr = 2: grant to 2 moves it to 3
- ptr = 3: grant to 3 moves it to 0
- BUG_SKIP at step 1: grant to 0 jumps ptr to 2; requester 1 has just raised its request
- ptr = 0 → ptr = 1: gnt 0
- ptr = 1 → ptr = 2: gnt 1
- ptr = 2 → ptr = 3: gnt 2
- ptr = 3 → ptr = 0: gnt 3
- BUG_SKIP at step 1 → ptr = 2: the extra arrow
The rotation property allows only the four solid arrows. The measured trace walks the extra one first.
Measured with smtbmc yices: FAIL at reported step 6, 0.5 s. Requester 1 asks from step 1 and is granted only after the three others.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer writes the exclusion check and the rule of no grant without a request. It knows fairness is needed too.
What Interviewers Listen For (Mid-Level)
A good mid-level answer adds rotation and bounded fairness under a hold assumption, and covers each grant. It explains why the induction proof of fairness needs k = 6, or PDR.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompare
- Formally Verifying a Round-Robin Arbiter
-
WhyWhy the Fairness Proof Needs k = 6L2 Mid-LevelL3 Senior
The safety properties of the fixed arbiter prove at k = 2, but fairness needs k = 6. Why?
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
Fairness is checked with bench counters that count how long each request has waited. In the induction step those counters may start at any value the property allows, including combinations no real run produces. A longer window, k = 6 here, rules those starts out, while PDR finds the needed invariant by itself.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F8.2.2: Find the Unfair DownstreamSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfWhat a Fixed-Priority Arbiter HidesL2 Mid-Level
Asked if they stop at the safety properties
A fixed-priority arbiter passes every safety check you wrote. What is it hiding?
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
Starvation: a low-priority requester can wait forever while higher ones keep asking. Safety properties cannot see that, because no single cycle is wrong. You need a liveness property under fairness, or a bounded wait under a named stand-in assumption. Take the bound for the wait from a measured cover.
BUG_FIXED_PRIO: input 1 waits while input 0 streams Measured,
bmcdepth 20: FAIL at reported step 8 ona_wait. 4 input-0 packets are accepted while input 1 waits.Self-Check
Tick each key point you covered in your answer.
-
CompareThe Same Arbiter in SimulationL1 JuniorL2 Mid-Level
How would simulation verify the same arbiter, and what would it be likely to miss?
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 random-request bench with a reference model and grant-latency checks finds most bugs quickly. What it misses are skips and starvation that need a specific multi-cycle pattern of requests. Random stimulus rarely produces that exact pattern. Formal finds such patterns in a few steps, which is why arbiters are a classic first formal target.
The counterexample SBY wrote for the arbiter A formal counterexample for an arbiter: three chosen inputs straight after reset give a double grant.
Self-Check
Tick each key point you covered in your answer.
-
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 People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Missed Corner
"One grant at a time and no grant without a request are enough."
This arbiter skips a requester that was idle last cycle, and both safety checks still pass. The bounded fairness check in the fix fails at step 6.
Run It
The skipping round-robin arbiter from lesson F8.2, checked only for one grant at a time and no grant without a request.
module rr4(input clk, rst, input [3:0] req, output reg [3:0] gnt);
reg [1:0] ptr = 0;
reg [3:0] req_q = 0; // last cycle's requests
reg [1:0] idx; // the granted index
integer i;
always @(*) begin
gnt = 0; idx = 0;
for (i = 3; i >= 0; i = i - 1) // the lowest offset from ptr wins
if (req[ptr + i[1:0]]) begin gnt = 4'b0001 << (ptr + i[1:0]); idx = ptr + i[1:0]; end
end
always @(posedge clk)
if (rst) begin ptr <= 0; req_q <= 0; end
else begin
req_q <= req;
if (gnt != 0) ptr <= req_q[idx + 2'd1] ? idx + 2'd1 : idx + 2'd2; // bug: skips a requester idle last cycle
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
// The requesters' promise: a request stays up until it is granted.
reg [3:0] gnt_q = 0;
always @(posedge clk) if (!rst) assume((req_q & ~gnt_q & ~req) == 0);
reg [2:0] wait0 = 0, wait1 = 0, wait2 = 0, wait3 = 0; // cycles each request has waited
always @(posedge clk) begin
gnt_q <= rst ? 4'd0 : gnt;
wait0 <= rst || !req[0] || gnt[0] ? 3'd0 : wait0 + 3'd1;
wait1 <= rst || !req[1] || gnt[1] ? 3'd0 : wait1 + 3'd1;
wait2 <= rst || !req[2] || gnt[2] ? 3'd0 : wait2 + 3'd1;
wait3 <= rst || !req[3] || gnt[3] ? 3'd0 : wait3 + 3'd1;
end
reg [1:0] ptr_exp = 0; // where the pointer must go: past the last grant
always @(posedge clk) if (!rst && gnt != 0) ptr_exp <= idx + 2'd1;
always @(posedge clk) if (!rst) begin
assert($onehot0(gnt)); // at most one grant
assert((gnt & ~req) == 0); // no grant without a request
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
See the Fix
module rr4(input clk, rst, input [3:0] req, output reg [3:0] gnt);
reg [1:0] ptr = 0;
reg [3:0] req_q = 0; // last cycle's requests
reg [1:0] idx; // the granted index
integer i;
always @(*) begin
gnt = 0; idx = 0;
for (i = 3; i >= 0; i = i - 1) // the lowest offset from ptr wins
if (req[ptr + i[1:0]]) begin gnt = 4'b0001 << (ptr + i[1:0]); idx = ptr + i[1:0]; end
end
always @(posedge clk)
if (rst) begin ptr <= 0; req_q <= 0; end
else begin
req_q <= req;
if (gnt != 0) ptr <= req_q[idx + 2'd1] ? idx + 2'd1 : idx + 2'd2; // bug: skips a requester idle last cycle
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
// The requesters' promise: a request stays up until it is granted.
reg [3:0] gnt_q = 0;
always @(posedge clk) if (!rst) assume((req_q & ~gnt_q & ~req) == 0);
reg [2:0] wait0 = 0, wait1 = 0, wait2 = 0, wait3 = 0; // cycles each request has waited
always @(posedge clk) begin
gnt_q <= rst ? 4'd0 : gnt;
wait0 <= rst || !req[0] || gnt[0] ? 3'd0 : wait0 + 3'd1;
wait1 <= rst || !req[1] || gnt[1] ? 3'd0 : wait1 + 3'd1;
wait2 <= rst || !req[2] || gnt[2] ? 3'd0 : wait2 + 3'd1;
wait3 <= rst || !req[3] || gnt[3] ? 3'd0 : wait3 + 3'd1;
end
reg [1:0] ptr_exp = 0; // where the pointer must go: past the last grant
always @(posedge clk) if (!rst && gnt != 0) ptr_exp <= idx + 2'd1;
always @(posedge clk) if (!rst) begin
assert(wait0 < 4 && wait1 < 4 && wait2 < 4 && wait3 < 4); // granted within four cycles
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 6
Misconception
"Write fairness as req |-> s_eventually gnt and run bmc."
No bounded run can show an endless wait, and without the hold assumption any request that drops breaks the property. Use the bounded form under the hold assumption, or a liveness engine with fairness.
Source IEEE 1800-2017 §16.12; Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 9 "Liveness properties that are not alive"