SystemVerilog Assertions interview preparation

SystemVerilog Assertions

Learn the sampling model, temporal operators, proof controls, and reusable protocol patterns through six connected concepts.

Curated and reviewed by industry engineersUpdated July 2026IEEE 1800 SystemVerilog reference

A request pulse opens a three-clock response window, ending at a marked deadline. — A request opens a window in time.

The language bench / assertions

Give the response a deadline.

Sampled clock 0RESET RELEASED

Cycle	0
req	0
ack	0
reset	0

No rising request has been exercised. There is no response evidence yet.

REQ at next clock

ACK at next clock

Controls stage the next sample. Reset acts between clocks. This scratch trace holds 24 clocks; Reset starts again.

pending0

passed0

failed0

aborted0

assert property (@(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:3] ack);
// ACK must be sampled 1, 2, or 3 cycles after REQ rises.

Question directory

Choose an interview question

Open a question at its supporting explanation. The complete property reference stays directly above each answer set.

Sampling modelWhat is SVA, and what does it add to SystemVerilog?Sampling modelHow do immediate and concurrent assertions differ?Sampling modelWhere does a concurrent assertion sample, evaluate, and run its action block?Sampling modelHow do $rose, $fell, $stable, and $past use sampled values?Sampling modelWhich SVA helper functions catch one-hot and unknown-state bugs?Assertion anatomyWhat is the difference between a sequence, a property, and an assertion directive?Assertion anatomyWhat does ## mean, and how do delay ranges behave?Assertion anatomyHow do and, or, intersect, throughout, and within compose sequences?Assertion anatomyHow does property-level logic differ from sequence composition?Assertion anatomyWhere can SVA live, and when should you bind a checker?Implication and timingWhat is the difference between |-> and |=>?Implication and timingDoes |=> prevent overlapping property attempts?Implication and timingWhat is vacuous success, and how do you expose it?Sequence operatorsHow do [*], [=], and [->] repetition differ?Sequence operatorsHow do you check that a pulse is at least two sampled clocks wide?Sequence operatorsHow do you require alert after err is high for two consecutive cycles?Sequence operatorsWhat does throughout guarantee?Sequence operatorsWhat do first_match and a sequence's ended method control?Reset and meaningful proofWhat exactly does disable iff do?Reset and meaningful proofHow do you enforce a quiet window after reset deassertion?Reset and meaningful proofHow do assert, assume, and cover differ in formal and simulation?Reset and meaningful proofHow do cover property, assertion coverage, and covergroups differ?Reset and meaningful proofWhen do strong semantics and fairness assumptions matter?Reset and meaningful proofHow do disable iff, accept_on, reject_on, and expect differ?Protocol patternsHow do you check an exact request-to-acknowledge contract?Protocol patternsHow do you guarantee every request is granted within three sampled cycles?Protocol patternsHow do you block a second request until the prior grant, and what do until and until_with change?Protocol patternsHow do you assert ready-valid stability under backpressure?Protocol patternsHow do you fail a ready-valid stall that lasts more than five cycles?Protocol patternsHow do you prove a grant never occurs without a request?Protocol patternsCan a local-variable SVA prove tagged matching and FIFO order?

SystemVerilog Assertions concept reference

Find a section

Sampling model

Reason from the sampled clock edge.

Separate simulation updates from assertion sampling, then explain exactly when a concurrent property observes, evaluates, and reports a result.

Open section

Assertion anatomy

Build the temporal sentence in layers.

Start with Boolean expressions, compose sequences across sampled clocks, turn them into properties, and finally choose assert, assume, or cover.

Open section

Implication and timing

Place the consequent on the intended edge.

Draw the trace first, mark the antecedent endpoint, and only then choose overlapped or nonoverlapped implication and any explicit delay.

Open section

Sequence operators

Know what repeats, and where the match ends.

Distinguish consecutive, nonconsecutive, and goto repetition, then combine sequences only when their start and endpoint contracts are clear.

Open section

Reset and meaningful proof

Make every pass mean something.

Control attempt lifetime with reset, expose vacuity with coverage, and state the assumptions that separate useful formal proof from an overconstrained result.

Open section

Protocol patterns

Decompose one interface contract at a time.

Check causality, bounded response, stability, exclusivity, and ordering separately so a failure points to one broken rule instead of one dense property.

Open section