Overview

Nearly every design-verification interview contains a write-the-assertion round: the interviewer states a protocol rule in English and watches you translate it into SVA on a whiteboard. The rules come from a small set of recurring families. If you can recognize the family, you already know which operators the solution needs — the rest is careful bookkeeping about edges, cycle counts, and reset.

Every drill in this topic follows the same discipline: restate the requirement precisely, decide edge or level for the antecedent, decide |-> vs |=>, pick the repetition/delay operators, add disable iff, then check the assertion against a pass trace and a fail trace cycle by cycle. Interviewers care more about that checking step than about getting the operator right on the first try.

Sub-topics

1. Handshake Drills — req/ack timing, stability until ack, no re-request, no orphan ack.

2. Pulse & Stability Drills — one-cycle pulses, min/max width, stability windows, mutual exclusion.

3. Sequence Pattern Drills — A-then-B-then-C, counted occurrences, B-before-C ordering, bit patterns.

4. Counting & Window Drills — outstanding-transaction bounds, grant latency, events-per-window, stall runs.

5. Data Integrity Drills — delayed-equality pipelines, FIFO matching with local variables, tag matching, write-readback.

6. Reset & X-Checking Drills — reset values, X-freedom after reset, deassertion deadlines, init ordering.

7. FSM & Arbiter Drills — legal transitions, onehot state, grant rules, fairness and starvation bounds.

8. SVA Anti-Patterns Review — the classic interviewer-bait mistakes, each with broken code, failing trace, and fix.

Legend: [SVA] [INTERVIEW]

  PICKING THE FAMILY FROM THE ENGLISH SENTENCE

  "X happens, then Y within N cycles"        ──► handshake / delay      ##N, ##[M:N]
  "X is high for exactly/at least K cycles"  ──► pulse width            [*K], [*M:N]
  "Y must not change while X"                ──► stability              $stable, throughout
  "A then B then C"                          ──► sequence ordering      [->1], ##, until
  "no more than N outstanding / in a row"    ──► counting               aux counter, [*N+1], not
  "output equals input N cycles ago"         ──► data integrity         $past, local vars
  "after reset, ..."                         ──► reset/X family         $rose(rst_n), $isunknown
  "only legal transitions / one grant"       ──► FSM & arbiter          inside, $onehot

  Then ALWAYS:
    edge or level antecedent?   ($rose vs raw level)
    same cycle or next?         (|-> vs |=>)
    bounded or unbounded?       (##[1:N] vs ##[1:$] — sim vs formal)
    disable iff (!rst_n)        (almost always yes)

How to answer at the whiteboard

1. Restate the rule with explicit cycle numbers: 'if req rises at cycle T, ack must be high at cycle T+3 exactly'.

2. Declare your antecedent edge/level choice out loud and why — this is where most candidates silently go wrong.

3. Write the property, then immediately draw a pass trace and a fail trace and step the assertion through both.

4. State what the assertion does NOT check (vacuous cases, reset, overlapping requests) before the interviewer asks.

Key takeaways

• Interview assertions come from ~8 recurring families — recognize the family, and the operators follow.

• Always make the edge-vs-level and |-> vs |=> decisions explicitly; they are the two most common error sources.

• Verifying your own assertion against a hand-drawn pass and fail trace is the skill being graded.