← Design Verification Interviews
Interview Question · Debug
One Request, One Failure, a Correct Design
The Question
The interviewer asks
The protocol says: req is a level held until ack, and ack must come 1 to 3 cycles after req rises. The design answered in the third cycle, yet the assertion failed once. Here is the log. Why?
cycle 1: req=1
cycle 2: req=1
cycle 3: req=1
cycle 4: req=1 ack=1 (answered in the third cycle: legal)
cycle 5: req=0 ack=0
cycle 7: a_ack failed // a_ack: req |-> ##[1:3] ackYou 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 antecedent req is a level, so a new attempt starts on every cycle req is high. Here that is four attempts for one request. The first three see the ack in their window. The attempt that started in cycle 4 has no ack left in cycles 5 to 7, so it fails. Write the antecedent as the event the spec means: $rose(req) |-> ##[1:3] ack.
One column per cycle. A level antecedent starts an attempt in every cycle that req is high.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer counts the attempts in the log and sees that only the last one fails. It then switches the antecedent to $rose(req).
What Interviewers Listen For (Mid-Level)
A good mid-level answer checks every implication for a level antecedent where the spec means an event. It adds a separate rule that req stays high until ack.
What Interviewers Listen For (Senior)
A good senior answer makes "edge or level?" a review question for every antecedent. False failures like this one teach people to ignore the checker.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompare
- One Request, One Failure, a Correct Design
-
WhyWhy an Attempt Starts at Every TickL1 Junior
Why does an assertion start a new attempt on every clock tick, even while an earlier attempt is still running?
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 rule such as "every request is answered" must hold for each request, wherever it happens. Starting at every tick means no request can slip past while an older attempt is busy. Ticks where the antecedent does not match end at once, so they cost almost nothing.
Self-Check
Tick each key point you covered in your answer.
Misconception
"A new attempt waits until the previous one finishes."
Attempts are independent and overlap freely. That is why overlapping requests are each checked.
Source IEEE 1800-2017 §16.14.1
-
What IfMany Attempts Open at OnceL1 JuniorL2 Mid-Level
What if a request arrives every cycle and each one takes 10 cycles to answer? How many attempts are open, and does it matter?
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
About ten attempts are open at any time, one per request in flight. Each keeps its own threads and local variables, which is correct and expected. On busy buses with long windows, this costs simulation time. If it is too slow, tighten the window, or check order in a scoreboard instead.
Self-Check
Tick each key point you covered in your answer.
Misconception
"An assertion handles one request at a time, so overlapping requests are skipped."
Each tick starts its own attempt, so every request gets its own check. None is skipped.
Source IEEE 1800-2017 §16.14.1
-
CompareLevel or Edge in the AntecedentL1 JuniorL2 Mid-Level
A request is held high until it is served. Why does
req |-> ##[1:3] ackfail on a design that answers every request in two cycles, and how does$rosefix it?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 level antecedent starts a new attempt at every edge where
reqis high. The attempts started late in a long request have windows that end after the singleack.$rose(req)starts exactly one attempt per request. Use a level only when every cycle of the level really owes its own response.Self-Check
Tick each key point you covered in your answer.
Half-Truth
"
$rosein the antecedent is just style."It changes the number of attempts. With a held request the level form makes one obligation per cycle, which the design never promised.
Source IEEE 1800-2017 §16.12.7
-
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.
-
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.
-
Break ItWhen Rose Misses a Second RequestL2 Mid-Level
How does the
$rose(req)fix break if a new request can start in the same cycle that the old one is acknowledged?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
If
reqstays high across the boundary between two requests, there is no rise for the second one. So it is never checked. For such protocols, start the attempt at "request accepted" or "first cycle of a new request", for examplereq && !$past(req) || (req && $past(ack)).Self-Check
Tick each key point you covered in your answer.
Missed Corner
"
$rosemarks the start of every request."It marks a change from 0 to 1 only. Back-to-back requests that keep the signal high produce no second rise.
Source IEEE 1800-2017 §16.9.3
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"The assertion checks each request once."
An attempt starts at every clock tick, and each tick with req high is a new request to the property. The twin starts four attempts and the last one fails.
Run It
One request held for four cycles, answered legally in the third.
cycle 7: a_ack failed failures=1 FAIL: a level antecedent starts a new attempt every cycle req is high; the last one had no ack leftSee the Fix
module tb;
logic clk = 0, req = 0, ack = 0;
int cyc = 0, fails = 0;
always #5 clk = ~clk;
always @(posedge clk) cyc <= cyc + 1;
// Protocol: req is a level, held until ack; ack must come 1 to 3 cycles after req rises.
a_ack: assert property (@(posedge clk) $rose(req) |-> ##[1:3] ack)
else begin fails++; $display("cycle %0d: a_ack failed", cyc); end
initial begin
@(negedge clk) req = 1; // one request, held
repeat (2) @(negedge clk);
@(negedge clk) ack = 1; // ack in the third cycle: legal
@(negedge clk) begin req = 0; ack = 0; end
repeat (4) @(negedge clk);
$display("failures=%0d", fails);
if (!fails) $display("PASS: one attempt per request, and the request was answered in time");
$finish;
end
endmodule
Prints: failures=0 PASS: one attempt per request, and the request was answered in time
Delivery
"The design is late; ack should come in the second cycle."
The log shows ack within three cycles of the rise, which the spec allows. Debug the checker against the spec before blaming the design.
Half-Truth
"Widen the window to ##[1:6] and the failure goes away."
That hides the false failure, but also allows a really late ack for the first attempt. The antecedent is wrong, not the window.