Answer each question out loud before opening it. If you miss more than three in the checkpoint, revisit the lessons linked at the end.
Numbered rules that can each become an assertion, stated freedoms and limits, corner cases covered, diagrams labelled as examples.
Liveness; bound it, check for leftovers at the end of the test, or prove it formally.
assert property (@(posedge clk) disable iff (!rst_n) valid && !ready |=> $stable(data));
It samples only on transfer cycles and closes the transaction on the protocol's end marker or final beat.
One queue of predictions per ordering domain (ID or tag); compare each response with the oldest in its own queue.
A protocol plan: handshake timing, outstanding counts, ordering, boundaries, errors, flow control, reset, crosses, every assertion's trigger.
For handshakes, counters, credit loops, FIFOs, arbiters, ordering and deadlock: rare combinations rather than data.
An independent reading of the standard, already exercised widely, with agent, checker, coverage and compliance tests.
Status and sticky errors, counters, timestamped trace frozen by triggers, and a debug path that works when hung.
Find the missing condition, the state behind it, check it with a conservation rule, go back to the first wrong cycle.
Task. You are handed DCLink (valid/ready hops, credits, tags 0 to 3, replay) to verify before tape-out. Lay out the verification plan: checks, models, coverage, formal targets, and what you would ask the designers to add for silicon debug.
Checks: a checker bound at every hop with hold, stable, known, bounded-length and bounded-response rules, plus credit conservation (occupancy + sender credits + credits in flight = depth) and sequence-number rules for replay. Models: passive monitors per hop rebuilding packets and completions; a reference model predicting read data; a scoreboard with one outstanding entry per tag (tags are unique while outstanding); end-of-test checks that nothing is outstanding and every replay buffer drained. Coverage: stalls of every length class, back-to-back, every outstanding count to 4 tags, reordering across tags, credits at zero, ACK and NAK paths, replay timeout, CRC error injection on first, middle and last flits, reset with traffic in flight, crosses such as NAK during credit starvation. Formal: handshake rules per hop, credit counters and conservation, the replay buffer's sequence window, the arbiter's bounded wait, and deadlock freedom of the message classes. Independence: checker and model written from the specification by someone other than the designer. Silicon debug: credit and outstanding counters, sticky CRC and replay error capture with sequence numbers, a trace buffer per hop frozen by a replay-timeout or completion-timeout trigger.
A diagram is one example; it does not say which features are required.
Safety: credits never exceed the buffer depth. Liveness: every sent packet's credit eventually returns.
Otherwise it may never have been triggered and proves nothing.
Turns the check off during reset so reset values cause no false failures.
Stalled words are counted several times.
It accepts illegal reorderings, wrong IDs and duplicates.
Puts it out of step, so later responses in that ID mismatch; report the first error.
Cover properties showing the interesting states are still reachable.
A checker and model written from the specification by someone other than the designer.
Credits + occupancy + owed = initial credits: 0 + 0 + 3 = 3, so credits were withheld, not lost.