SVA interviews have two rounds. The whiteboard round states a protocol rule in English and asks for the assertion. The verbal round asks what the operators mean and why an assertion disagrees with a waveform.
Each drill page gives three prompts and one starter bench. You write the assertions, run the bench, and read the grader before you see any answer. The grader runs legal traffic, where your assertions must stay silent, then one planted bug per drill, which yours must report: an answer that is too strict and an answer that is too loose both fail.
Every drill in this topic follows one discipline. Restate the rule with cycle numbers, choose edge or level aloud, pick the implication, then step the property through a pass trace and a fail trace.
Restate the rule with explicit cycle numbers: if req rises at cycle T, ack is high at cycle T+3 exactly.
Declare the antecedent edge or level choice out loud and why.
Write the property, then draw a pass trace and a fail trace and step through both.
State what the assertion does not check: vacuous cases, reset, overlapping requests.
The sentence says | Family | Tools |
|---|---|---|
X happens, then Y within N cycles | Handshake and delay |
|
X is high for exactly or at least K cycles | Pulse width | Written-out runs, |
Y must not change while X | Stability |
|
A, then B, then C | Ordering |
|
No more than N outstanding, or N in a row | Counting | A counter in modeling code |
Output equals input N cycles ago | Data integrity |
|
After reset, ... | Reset | Modeling flops that reset with the design |
Only legal transitions, one grant | FSM and arbiter |
|
Then decide four things aloud: edge or level antecedent ($rose or the raw level), same cycle or next (|-> or |=>), bounded or unbounded (##[1:N] for simulation), and disable iff on reset (almost always).
Lesson | You will drill… |
|---|---|
Exact and windowed req/ack latency, stability until ack, no re-request, no orphan ack. | |
Single-cycle pulses, bounded widths, stable-while-enabled data, glitch windows, mutex rules. | |
Bounded A-then-B ordering, goto versus nonconsecutive repetition, windowed counts, aux counters. | |
Pipeline delay checks, tag matching, write-readback rules, reset values, X contracts. | |
Legal transitions, onehot state, per-bit grant rules, round-robin ordering. | |
Immediate versus concurrent, sampling, attempts, assert/assume/cover, naming. | |
Implication anchors, delay ranges, repetition endpoints, window operators, first_match. | |
Vacuous passes, cover pairing, weak versus strong, debug triage, formal semantics. |
When an assertion fails on good RTL, or passes on broken RTL, one of seven classic mistakes is usually behind it.
Fails a known-good design at txn end, off by one cycle: implication off-by-one.
One pass then N-1 fails per transaction (a fail for every extra cycle the level stays high), attempt counts explode: level retrigger.
Failures clustered at reset events: missing disable iff.
Dead handshake but regression green: weak unbounded liveness.
Late event accepted silently: [=N] absorbing the slack.
False fail when the trigger window has several matches: missing first_match.
False fail right after reset or between beats: ungated $past.
Edge or level for the antecedent ($rose, since one rise is one obligation), the implication (|-> with ##3, since the rise cycle plus 3 is the target), and the reset clause (disable iff, since this is a functional check).