← Design Verification Interviews
Interview Question · Design
Checking an Arbiter
The Question
The interviewer asks
Design the assertion set for a three-way round-robin arbiter. Which rules are safety, which are fairness, and which ones can simulation really check?
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
Safety rules: at most one grant, written $onehot0(gnt), and grants only to requesters, written (gnt & ~req) == 0. A third safety rule: a request is not granted while it is low. Fairness: a waiting request is granted within N cycles, where N follows from the round-robin order. Simulation checks the bounded form well. The unbounded form, "eventually granted", needs a formal tool or a strong property at the end of the test.
Read the diagram as text
- Round-robin arbiter: req[2:0] in, gnt[2:0] out
- Safety: one grant: $onehot0(gnt)
- Safety: grant to a requester: (gnt & ~req) == 0
- Fairness, bounded: A waiting request is granted within N cycles
- Liveness, unbounded: Every request is eventually granted
- Simulation: Fails at the exact cycle the rule breaks
- Formal tool: Proves it for every request pattern
- Round-robin arbiter → Safety: one grant
- Round-robin arbiter → Safety: grant to a requester
- Round-robin arbiter → Fairness, bounded
- Round-robin arbiter → Liveness, unbounded
- Safety: grant to a requester → Simulation: checked well
- Fairness, bounded → Simulation: checked well
- Liveness, unbounded → Formal tool: needs a proof
Safety and bounded fairness fail at one cycle, so simulation checks them well. The unbounded form needs formal, or a strong property at the end of the test.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Mid-Level)
A good mid-level answer writes the one-grant rule and the grant-to-a-requester rule. It turns fairness into a wait with a fixed limit.
What Interviewers Listen For (Senior)
A good senior answer works out N from the round-robin scheme. It explains why the bounded rule is the sign-off property, and leaves the unbounded one to formal.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompareScale It
- Checking an Arbiter
-
WhyWhy Fairness Becomes a Bounded WaitL2 Mid-Level
Why turn "every request is eventually granted" into "granted within N cycles"?
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 finite, so "eventually" can only fail at the very end, and only in its strong form. A bounded wait fails at the exact cycle the promise breaks, which is much easier to debug. For round-robin, N is about the number of other requesters times their longest grant.
Self-Check
Tick each key point you covered in your answer.
Misconception
"Bounded waits are weaker, so they miss bugs."
The bound is stronger: a design that grants late but eventually passes "eventually" and fails the bound.
Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §20.1
-
What IfA Fairness Bound with Long GrantsL2 Mid-LevelL3 Senior
What if requesters may hold a grant for up to 8 cycles? How do you work out N for four requesters?
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
N is the worst wait: every other requester gets one grant before you, each held for its longest time. With four requesters that is about 3 × 8 cycles, plus the arbiter's own latency. If the hold time has no limit, no bound exists. Then the spec needs a hold-time rule first.
Self-Check
Tick each key point you covered in your answer.
Half-Truth
"N is just the number of requesters."
That assumes every grant lasts one cycle. Long grants by the others add their hold time to the wait.
-
CompareOnehot vs Onehot0L1 Junior
Compare
$onehot(v),$onehot0(v)and$countones(v) <= 1.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
$onehot(v)is true when exactly one bit is 1.$onehot0(v)is true when at most one bit is 1, so all zeros pass.$countones(v) <= 1means the same as$onehot0and is clearer when the limit is not one.v$onehot(v)$onehot0(v)$countones(v) <= 13'b000 0 1 1 3'b010 1 1 1 3'b011 0 0 0 Only the all-zero value separates
$onehotfrom the other two.Self-Check
Tick each key point you covered in your answer.
Misconception
"
$onehot0means one-hot with bit 0 excluded."The 0 means zero bits set is also allowed. No bit position is special.
Source IEEE 1800-2017 §20.9
-
Scale ItFormal Sign-Off for an ArbiterL3 SeniorL4 Staff
For the chip's main interconnect arbiter, simulation passes. What would you add before sign-off, and 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
Run the same safety and bounded-fairness assertions in a formal tool, with assumptions only for real protocol rules on the requesters. Formal explores every request pattern, including the rare one where two masters starve a third. Then check that the covers are reachable, so the proof is not empty. Simulation alone samples a small part of that space.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Senior)
A good senior answer names the starvation pattern that simulation rarely hits. It demands reachable covers along with the proof.
What Interviewers Listen For (Staff)
A good staff answer weighs the formal effort against the risk of this arbiter. It sets the sign-off rule for every shared arbiter on the chip.
Half-Truth
"A long random regression is as good as a proof."
Random traffic rarely hits the exact patterns that starve one requester. Formal checks all patterns within its bound.
-
Prove ItSolve 6.6.8: Answer in TimeSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"$onehot(gnt) says there are never two grants."
$onehot demands exactly one bit set, so every idle cycle fails. The twin fails three idle cycles of a correct arbiter.
Run It
A correct arbiter with idle cycles, checked with $onehot.
grant check failures=3 FAIL: $onehot demands exactly one grant, so every idle cycle failedSee the Fix
module tb;
logic clk = 0;
logic [2:0] req = 0, gnt = 0;
int fails = 0;
always #5 clk = ~clk;
// The fix: at most one grant, and only to a requester.
a_grant: assert property (@(posedge clk) $onehot0(gnt) && ((gnt & ~req) == 0)) else fails++;
initial begin
@(negedge clk) begin req = 3'b011; gnt = 3'b001; end
@(negedge clk) begin req = 3'b000; gnt = 3'b000; end // idle: nobody asks, nobody is granted
@(negedge clk) begin req = 3'b000; gnt = 3'b000; end
@(negedge clk);
$display("grant check failures=%0d", fails);
if (!fails) $display("PASS: idle cycles with no grant are legal");
$finish;
end
endmodule
Prints: grant check failures=0 PASS: idle cycles with no grant are legal
Half-Truth
"Fairness means every requester gets the same number of grants."
Equal counts depend on the traffic. The checkable promise is a bounded wait for each waiting request.
Buzzword Without Mechanism
Writes "eventually granted" with ##[1:$] and calls fairness checked.
In an assert that form is weak and never fails in simulation. It checks nothing unless it is strong or bounded.
Source IEEE 1800-2017 §16.12.2