← Design Verification Interviews
Interview Question · Code Writing
Writing Valid Holds Until Ready
The Question
The interviewer asks
Write an assertion for the rule "once valid is high, it must stay high until ready is high". A candidate wrote the line below. Does it check the rule?
assert property (@(posedge clk) valid |-> ##[0:$] ready);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
No. It only says that some ready comes later, and with no deadline it can never fail in a finite test. It never checks valid in the cycles between. Write the rule cycle by cycle: valid && !ready |=> valid. Every cycle where the offer waits, the next cycle must still show valid.
One column per rising edge; here the signals are rvalid and rready. The rule rvalid && !rready |=> rvalid fails at edge 3, where the offer drops. The data arrives later, so a scoreboard is satisfied.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Fresher)
A good fresher answer sees that the candidate's line never looks at valid after the first cycle. It then writes the cycle-by-cycle rule.
What Interviewers Listen For (Junior)
A good junior answer adds the matching data rule, valid && !ready |=> $stable(data). It also adds a reset guard.
What Interviewers Listen For (Senior)
A good senior answer puts the rule in the interface, so every link gets it. It adds a deadline for ready only if the protocol promises one.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompare
- Writing Valid Holds Until Ready
-
WhyWhy an Open-Ended Wait Cannot FailL1 JuniorL2 Mid-Level
Why can
valid |-> ##[0:$] readynever fail in simulation?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 window has no end, so there is always a later cycle where
readymight still arrive. In anassert, an attempt that is still waiting when the test ends counts as weak, so it does not fail. Only a strong form, such ass_eventually, fails when the test ends first.Self-Check
Tick each key point you covered in your answer.
Spec Misquote
"It fails at the end of the test if ready never came."
A sequence property in an assert is weak by default, so an unfinished attempt is not a failure.
Source IEEE 1800-2017 §16.12.2
-
What IfChoosing the Bound for ReadyL1 JuniorL2 Mid-Level
What if you replace the open window with a bound? What number do you pick, and where does it come from?
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
Take it from the spec or the slave's datasheet, such as a maximum number of wait states. If the spec gives none, agree a system timeout with the architect and write it down. Use
valid |-> ##[0:N] ready. Then cover the longest legal wait, so tests reach the bound.Self-Check
Tick each key point you covered in your answer.
Half-Truth
"Pick N = 1000 so it never fires falsely."
A huge bound hides a slow slave and reports a hang far from its cause. The bound should come from a spec number.
-
CompareA Cycle Rule vs Until_with for One HandshakeL1 JuniorL2 Mid-Level
Compare
valid && !ready |=> validwith$rose(valid) |-> valid until_with ready.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
Both catch a withdrawn offer. The cycle rule starts a short attempt on every waiting cycle, so it is easy to read and runs on every tool. The
until_withform starts one attempt per offer and follows it to the handshake. It misses offers that start whilevalidis already high, such as back-to-back beats.valid && !ready |=> valid$rose(valid) |-> valid until_with readyAttempts One per waiting cycle One per offer A withdrawn offer Caught Caught Back-to-back beats Every waiting beat is checked A beat that starts while validis high gets no attemptSelf-Check
Tick each key point you covered in your answer.
Missed Corner
"
$rose(valid)catches every new offer."Back-to-back beats keep
validhigh, so there is no rise for the second offer. That offer is never checked.Source IEEE 1800-2017 §16.9.3
-
Prove ItSolve 6.6.6: Hold the OfferSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Break ItA Hold Rule That Never StartedL1 JuniorL2 Mid-Level
The hold rule passed across the whole regression. Why might that prove nothing?
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
Its antecedent needs a stalled offer. If every test drives
readyhigh, no attempt ever reaches the consequent, and the zero-failure report is vacuous. Count or covervalid && !readyand make a stalling sink part of the agent.Self-Check
Tick each key point you covered in your answer.
Half-Truth
"Vacuous passes only come from typos."
Here the property is correct; the stimulus never creates the situation it checks.
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"valid |-> ##[0:$] ready says valid stays high until ready."
The range only waits for a later ready; it says nothing about valid meanwhile. The twin withdraws valid early and the rule reports 0 failures.
Run It
A source that withdraws its offer before ready, checked by the candidate's rule.
failures=0 FAIL: the rule only waits for some later ready; it never checked that valid stayed highSee the Fix
module tb;
logic clk = 0, valid = 0, ready = 0;
int fails = 0;
always #5 clk = ~clk;
// The fix: once offered and not taken, valid must still be high at the next edge.
hold_rule: assert property (@(posedge clk) valid && !ready |=> valid) else fails++;
initial begin
@(negedge clk) valid = 1; // offered, not taken
@(negedge clk) valid = 0; // withdrawn before ready: illegal
repeat (3) @(negedge clk);
@(negedge clk) begin valid = 1; ready = 1; end
@(negedge clk) begin valid = 0; ready = 0; end
repeat (2) @(negedge clk);
$display("failures=%0d", fails);
if (fails) $display("PASS: the hold rule caught the withdrawn offer");
$finish;
end
endmodule
Prints: failures=1 PASS: the hold rule caught the withdrawn offer
Misconception
"Use |-> instead of |=>; it is the same rule."
valid && !ready |-> valid checks the same cycle, where valid is already true. It can never fail.
Source IEEE 1800-2017 §16.12.7
Missed Corner
Writes only the valid rule and forgets the data.
A source can hold valid and still change the data during the stall. The protocol needs both rules.
Source AMBA AXI Protocol Specification IHI 0022L §A2.3 Valid-Ready transport