Articles

SystemVerilog Assertion Interview Questions: Implication, Sampling, and Vacuity

Prepare for SystemVerilog Assertion interviews with implication timing, sampled values, reset aborts, vacuous success, past-value history, and coverage.

A passing assertion can mean that the required behavior occurred, that its trigger never occurred, or that you are reading the tool's report incorrectly. SystemVerilog Assertion interview questions test whether you can connect a property to sampled signals and a precise requirement, rather than treating a green summary as complete verification.

Official reference boundary: IEEE lists SystemVerilog's language standard as IEEE 1800-2023. The explanations here use an Accellera-hosted assertion tutorial and linked, firsthand expert commentary; that commentary is not itself the normative standard. Original traces and recommendations are labelled separately. No candidate reports or employer question-frequency claims are used. Check the language edition and your simulator's supported assertion features. IEEE standard listing, Accellera SVA tutorial

What contract should you state before writing a property?

Start with the clock, reset, trigger, allowed response window, and transaction identity. These original requirements sound similar but require different checks:

Every cycle with req high requires ack on that same sampled edge.
Each rising transition of req requires ack on the next sampled edge.
Every accepted request requires a matching response within three cycles.

The third requirement cannot be reduced to the second without defining acceptance and matching. If requests carry IDs, one acknowledgement level may not identify which request completed. If a request is held high while waiting, treating every high cycle as a new transaction can create obligations the interface never intended.

Engineering recommendation: translate the English requirement into a small accepted-event ledger first. Ask whether reset cancels outstanding obligations and whether acknowledgement means “high sometime,” “a rising edge,” or “a response transfer.” A syntactically legal property can verify the wrong interpretation.

How do overlapping and non-overlapping implication differ?

For the single-clock, one-cycle Boolean antecedents in this guide, req |-> ack checks ack on the request's sampled edge; req |=> ack checks it on the following sampled edge. For a longer antecedent sequence, reason from the end of its match. Do not apply a simple one-cycle rewrite indiscriminately to all sequence forms. Accellera implication tutorial, Expert discussion of implication and equivalence limits

These original fragments use scalar req and ack, a single clock, and active-low reset:

assert property (@(posedge clk) disable iff (!rst_n)
  req |-> ack);

assert property (@(posedge clk) disable iff (!rst_n)
  req |=> ack);

assert property (@(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] ack);

The ranged version permits acknowledgement one, two, or three sampled edges after the trigger. It excludes the trigger edge. These fragments express different specifications; the task is not to choose the one that produces the fewest failures.

Original sampled trace: reset is inactive throughout, values are known 0/1, and the trace continues through edge 8:

Edge	req	ack	Relevant event
1	0	0	No request trigger
2	1	0	First request
3	0	1	Acknowledgement one edge later
4	0	0	Idle
5	1	1	Second request and same-edge acknowledgement
6	0	0	No next-edge acknowledgement
7	0	0	No acknowledgement
8	0	0	Three-edge window ends

Trigger edge	Same-edge property	Next-edge property	One-to-three-edge property
2	Fails at 2	Passes at 3	Passes using 3
5	Passes at 5	Fails at 6	Fails after window ends at 8

The acknowledgement at edge 5 does not satisfy that trigger's one-to-three-edge window. Explain the attempted property and its deadline together; a bare “ack went high” loses the relevant timing.

Why might the waveform or failure message seem contradictory?

For ordinary concurrent assertions clocked at posedge clk, operands are sampled before the edge's active updates; property evaluation and its action block occur in later simulation regions. An action block's ordinary signal reference uses its current value, which can differ from the sampled value used by the assertion. Accellera sampling tutorial, Dave Rich on sampled operands and action blocks

Original debugging case: ack is 0 immediately before an edge. An always_ff schedules ack <= 1 on that edge. A same-edge property checking sampled ack still sees 0. A later print of current ack may show 1. There is no contradiction once you label the regions.

Use sampled values in the failure diagnostic:

assert property (@(posedge clk) disable iff (!rst_n)
  req |-> ack)
else $error("sampled req=%0b ack=%0b",
            $sampled(req), $sampled(ack));

This is an original diagnostic example. Capture time, clock, reset, and sampled values with the failing attempt. A waveform view that hides delta-cycle changes can make two different values appear to occupy the same instant. Expand the event evidence before moving an implication operator to silence the message.

Clocking-block input skews have their own sampling contract. If the checker references a clocking block rather than raw interface signals, verify that contract explicitly instead of assuming every named signal represents the same sampling point.

Does disable iff merely skip a clock edge?

Expert explanation: when disable iff becomes true, active attempts terminate as disabled, neither passed nor failed. Its ordinary condition uses current, unsampled values and is asynchronous with respect to the property clock. It is not simply another sampled antecedent. Dave Rich on disable iff, Sampled validity versus asynchronous disabling

Original reset exercise: a request at edge 2 requires an acknowledgement at edge 4. Reset asserts between edges 3 and 4. With an appropriate disable iff (!rst_n), that pending attempt is aborted. Deasserting reset does not resume the old attempt and demand its postponed acknowledgement.

Contrast that with gating the clock event using iff. Suppressing a checking event is not the same as terminating an already active property attempt. State which reset behavior the specification actually requires.

A synchronous “check only when valid” condition often belongs in the sampled property expression. Do not casually put an ordinary synchronous enable into disable iff and expect it to behave like a sampled guard. Expert review of synchronous conditions

If reset changes in the same time slot as the clock, sampled reset and current reset can differ. Reproduce that scheduling case with the actual simulator before asserting that a screenshot alone establishes the cause.

What is vacuous success, and why should you care?

For implication, an antecedent that does not match can produce vacuous success: the consequent was not exercised by that attempt. This is different from a triggered obligation that was satisfied. Expert implication discussion

Original failure of evidence: the driver is incorrectly connected and req remains 0 for the whole test. req |-> ##[1:3] ack produces no meaningful response challenge. A “zero assertion failures” summary cannot tell you that the request path worked.

Keep the evidence states separate:

Reported situation	What it establishes	What is still missing
Antecedent never matches	No triggered response violation	Evidence of a request
Triggered attempt succeeds	That attempt met its property	Broader stimulus and matching correctness
Reset terminates the attempt	Disable policy applied	Completed pre-reset response behavior
Attempt is still pending	Its deadline has not resolved	An outcome after sufficient observation

Add coverage for the actual trigger and the desired sequence, without implication in these simple cover expressions:

cover property (@(posedge clk) disable iff (!rst_n) req);
cover property (@(posedge clk) disable iff (!rst_n)
  req ##[1:3] ack);

The first asks whether a sampled request occurred. The second seeks the request-followed-by-response pattern. Coverage display and vacuous-pass reporting vary by tool and settings; inspect the categories rather than assuming one green hit count excludes vacuity. Expert coverage discussion

These covers are evidence of exercised scenarios, not proof of all legal traces. Also test a deliberate bad response to confirm that the assertion can detect the error it claims to check.

When should you use req versus $rose(req)?

A level antecedent can create an obligation on every sampled high cycle. For a scalar signal, a rising-edge trigger selects a transition rather than each high sample. That difference must follow the interface requirement, not a desire to reduce checker activity. Expert sampled edge-function discussion

Original example: req remains high for three clocks while waiting for ack. A level-triggered next-edge assertion challenges three sampled cycles. A rising-edge version challenges only the initial transition. Neither automatically represents “one accepted transaction” unless the protocol defines that transition as acceptance.

With overlapping requests, a simple “ack becomes high in the window” property does not enforce one response per request. The same acknowledgement can satisfy multiple obligations. If that is forbidden, add transaction association, outstanding-count rules, or a scoreboard that represents the real protocol.

For vector inputs, do not treat $rose(vector) as a substitute for “any bit changed.” Define whether the requirement concerns one control bit, the whole value, or a particular transition, then choose the appropriate expression.

Why can $past fail near startup or reset?

$past refers to sampled history, not an arbitrary continuous interval before the current time. If sufficient previous sampling events do not exist, default sampled values matter. Ben Cohen on $past and history guards

Original one-cycle register example: suppose q captures d on each active edge. Check the relation only once post-reset sampled history is available:

logic history_valid;
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) history_valid <= 1'b0;
  else        history_valid <= 1'b1;

assert property (@(posedge clk) disable iff (!rst_n)
  history_valid |-> q == $past(d));

This is a checker fragment for the stated unconditional register contract, not a complete design. At the first post-reset edge, sampled history_valid is still 0, so the comparison is not challenged. At the next edge, q should reflect the preceding captured d.

For deeper or gated history, define the number and kind of samples required. A generic elapsed-time counter may not match a $past expression whose sampling is gated. Also decide whether reset should clear your history-valid bookkeeping; otherwise a later reset can expose pre-reset history as if it belonged to the new operation.

What makes an assertion review interview-ready?

Engineering recommendation: review one property with four traces: a valid triggered response, a violated deadline, a never-triggered case, and reset during an active attempt. Then add overlapping requests and unknown values according to the design's actual startup contract. Keep the main known-value trace separate from X/Z analysis.

Check end-of-test behavior. A test that ends immediately after a request can leave future obligations unresolved. Drain the relevant window and inspect pending-attempt handling; “no failure before stopping” does not establish future response behavior.

For formal work, distinguish an asserted guarantee from an assumed environment constraint. A three-cycle response deadline needs an architectural reason or explicit assumptions about downstream service. Over-constraining the environment until every property passes can remove the very counterexample you needed to find.

Record the clock, reset semantics, antecedent occurrence, non-vacuous evidence, and tool options beside the result. The fragments here are source-reviewed teaching examples; run them in the intended simulator before treating them as an integrated checker.