What First Match Changes

Where the interviewer goes next. Open a node to practise that follow-up.

WhyWhat IfBreak ItCompare

1. What First Match Changes
2. CompareFirst Match vs Two Assertions Keyed on the EventL2 Mid-Level

   Compare req |-> first_match(##[1:3] ack) ##1 done with the pair req |-> ##[1:3] ack and ack |=> done.

   Reveal the Model Answer

   The pair is close but not the same. ack |=> done demands done after every ack, including the second pulse. The first_match form only cares about the first one. If every ack really owes a done, the pair is simpler, easier to debug and runs on every simulator. If later pulses must not owe one, you need the first_match form or a small model that marks the first ack.

   	first_match form	ack |=> done pair
   Which acks owe a done	Only the first one	Every one
   Debug	One property to read	Each half reports on its own
   Runs on every simulator	No	Yes

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 The pair is close but not the same. Key point 2 ack |=> done demands done after every ack, including the second pulse. Key point 3 The first_match form only cares about the first one. Key point 4 If every ack really owes a done, the pair is simpler, easier to debug and runs on every simulator. Key point 5 If later pulses must not owe one, you need the first_match form or a small model that marks the first ack.

   Half-Truth

   "The two forms are always equivalent."

   They differ when ack can pulse more than once per request, which is exactly the case first_match was used for.

   Source IEEE 1800-2017 §16.9.8

   • Lesson A2.1Delays and Ranges: One Attempt, Many Threads
3. WhyWhy First Match Matters in an AntecedentL3 Senior

   Why does first_match matter even more in an antecedent, as in first_match(req ##[1:3] gnt) |=> busy?

   Reveal the Model Answer

   Each end point of the antecedent starts its own check of the consequent. Without first_match, two grants inside the window start two obligations for one request, so busy is demanded after each. first_match keeps one end point per start and one obligation per request.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Each end point of the antecedent starts its own check of the consequent. Key point 2 Without first_match, two grants inside the window start two obligations for one request, so busy is demanded after each. Key point 3 first_match keeps one end point per start and one obligation per request.

   Misconception

   "A ranged antecedent starts one check per attempt."

   It starts one check per end point of the antecedent match, which can be several per attempt.

   Source IEEE 1800-2017 §16.12.7

   • Lesson A1.3Implication and Vacuous Success
4. Break ItFirst Match That Turns a Pass into a FailureL3 Senior

   Break it: show a consequent where adding first_match turns a pass into a failure.

   Reveal the Model Answer

   Take req |-> ##[1:3] gnt ##1 busy. Without first_match, the attempt passes if any grant in the window is followed by busy. With first_match(##[1:3] gnt) ##1 busy, only the first grant counts. If busy follows the second grant but not the first, the first form passes and the second fails.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Take req |-> ##[1:3] gnt ##1 busy. Key point 2 Without first_match, the attempt passes if any grant in the window is followed by busy. Key point 3 With first_match(##[1:3] gnt) ##1 busy, only the first grant counts. Key point 4 If busy follows the second grant but not the first, the first form passes and the second fails.

   Misconception

   "first_match only matters for performance."

   It changes which end points exist. In a consequent, fewer end points can turn a pass into a failure.

   Source IEEE 1800-2017 §16.9.8

   • Lesson A1.3Implication and Vacuous Success
5. What IfWhy One Match Ends the AttemptL1 Junior

   Asked if they ask about ranges at the end of a consequent

   Why does the implication stop at the first match of busy[*2:4] instead of checking the longest one?

   Reveal the Model Answer

   A property built from a sequence asks whether the sequence can match. The implication succeeds as soon as one consequent match exists. Longer matches add nothing to that answer. Anything that must happen after the match has to be written as more sequence or as a separate rule.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 A property built from a sequence asks whether the sequence can match. Key point 2 The implication succeeds as soon as one consequent match exists. Key point 3 Longer matches add nothing to that answer. Key point 4 Anything that must happen after the match has to be written as more sequence or as a separate rule.

   Misconception

   "The simulator picks the longest match, like a greedy regular expression."

   There is no greedy choice; the property holds if any match exists, and the earliest one already proves it.

   Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §8.8 (PDF p142)

   • Lesson A2.2Repetition and Counting Events
6. Break ItA First Match Rule That Never FailsL2 Mid-Level

   Your first_match rule has passed every regression for months. How do you find out whether it can fail at all?

   a_first: 0 failures in 2,431 tests
   (no directed test violates the first-ack rule)

   Reveal the Model Answer

   Write a small directed test whose traffic must break the rule: here, an ack at +1 with done only at +3. Check that the assertion reports exactly that failure. If it does not, the tool is not evaluating the construct and the months of passes are worthless. This negative control belongs next to every non-trivial property.

   Self-Check

   Tick each key point you covered in your answer.

   Key point 1 Write a small directed test whose traffic must break the rule: here, an ack at +1 with done only at +3. Key point 2 Check that the assertion reports exactly that failure. Key point 3 If it does not, the tool is not evaluating the construct and the months of passes are worthless. Key point 4 This negative control belongs next to every non-trivial property.

   Wrong Altitude

   "Mutating the design is the only way to test an assertion."

   A directed must-fail stimulus is often enough, much cheaper, and exactly targets the construct in doubt.

   • Lesson A8.1Capstone: An Assertion Suite