SystemVerilog Assertions (SVA)Concepts and Interview QuestionsYou Should Master

SVA stands for SystemVerilog Assertions. It adds executable Boolean and temporal properties that can check design behavior in simulation and formal analysis, and can record that meaningful scenarios occurred.

A simple immediate assertion executes like a procedural if statement when control reaches it. A concurrent assertion starts attempts on a declared clocking event and evaluates sampled behavior over time.

At its clocking event, a concurrent assertion samples referenced design values in Preponed, evaluates the property in Observed, and schedules its pass or fail action block in Reactive.

They compare values sampled on the property clock. $rose and $fell detect a 0-to-1 or 1-to-0 transition of the expression's least significant bit, $stable checks that the sampled expression did not change, and $past(expr, n) returns its sampled value n clocking events earlier.

$onehot(expr) requires exactly one asserted bit, $onehot0(expr) permits zero or one, $isunknown(expr) detects any X or Z, and $countones(expr) returns the number of one bits. They turn common structural invariants into readable checks.

A sequence describes a temporal match. A property turns that match into a Boolean obligation, often with implication, reset, or logical composition. A directive such as assert, assume, or cover tells a tool what to do with the property.

The ## operator concatenates sampled sequence elements by clock ticks, not simulator time units. ##n selects an exact sampled delay, while ##[m:n] permits a match at any sampled delay in the inclusive range.

or accepts a match from either operand. Sequence and starts both operands together and may finish when the later one ends. intersect also requires both operands to start together, but it requires the same endpoint. throughout and within constrain one sequence across another sequence's span.

Sequence operators such as and, or, and intersect combine temporal matches and therefore have start and endpoint semantics. Property-level not, and, or, and if...else combine truth-valued property expressions. The spelling can look similar, but the object being combined is different.

Sequences and properties can be declared in modules, interfaces, programs, clocking blocks, packages, or compilation-unit scope where the language permits them. A bound checker attaches verification logic to a module type or instance without editing the RTL, which keeps reusable interface contracts separate from implementation code.

Overlapped implication, |->, starts the consequent at the antecedent endpoint. Nonoverlapped implication, |=>, starts the consequent on the sampling event after the antecedent ends.

No. Nonoverlapped describes where one attempt's consequent starts. Every matching antecedent can still launch another independent attempt on a later clock, even while an earlier attempt is pending.

An implication succeeds vacuously when its antecedent does not match, because no consequent obligation was created. Add cover properties for the trigger and representative end-to-end matches so a green assertion is not mistaken for exercised behavior.

Consecutive repetition [*] requires adjacent sampled matches. Nonconsecutive repetition [=] counts possibly gapped occurrences and permits trailing nonmatch cycles in the sequence match. Goto repetition [->] also permits gaps, but the final occurrence ends the match.

Trigger once on the rising edge and require the signal to remain high on the next sampled clock. Because the signal is already high on the trigger sample, $rose(p) |=> p establishes a minimum width of two sampled clocks.

Put the two-cycle err sequence in the antecedent, then imply alert on the following cycle. If the rule should fire once per contiguous err run, begin the antecedent with $rose(err).

expr throughout seq requires expr to remain true on every sampled tick occupied by the selected match of seq. It constrains the complete sequence span, including its endpoint.

first_match(seq) keeps only the earliest complete match when a sequence has several legal endpoints. seq.ended is true on the sampled clock where that named sequence reaches a match endpoint, which lets another sequence align to completion rather than to the start.

disable iff asynchronously disables a property while its expression is true and aborts active attempts without a pass or failure. The disable expression uses current values, not the sampled values used by the property body.

Trigger on the sampled rising edge of active-low reset and use nonoverlapped implication when the quiet interval begins on the following sampled clock. Then repeat the required idle condition for the exact number of protected samples.

assert checks a required property. assume constrains legal environment behavior for the analysis context. cover asks whether an interesting property can occur. Formal tools explore all traces allowed by assumptions, while simulation checks only the traces that ran.

cover property records that a Boolean or temporal sequence completed. Assertion coverage reports whether checker attempts started, passed, failed, or were vacuous. Covergroups sample value bins and crosses. Together they answer reachability, checker exercise, and data-space coverage questions.

They matter when a property requires an eventual future match. A weak unbounded obligation can remain unfinished at the end of simulation, while formal liveness may need a justified fairness assumption to rule out an environment that postpones progress forever.

disable iff aborts an active property attempt without pass or failure. accept_on and reject_on terminate evaluation by forcing success or failure when their condition becomes true; sync_accept_on and sync_reject_on make that decision on the property's sampling event. An expect statement is a procedural concurrent assertion that blocks its process until the property succeeds or fails.

Split the contract into an exact response edge, response pulse shape, and admission rule. Separate properties produce clearer failures and let the interface decide whether a new request is legal on the acknowledgement edge.

Trigger once on the request edge and allow a grant on any of the next three sampled edges: $rose(req) |-> ##[1:3] $rose(gnt). Use ##[0:3] if same-edge grant is legal. This checks latency, not transaction ownership.

Assert admission separately from response timing. $rose(req) |=> !$rose(req) until_with $rose(gnt) forbids a new request through and including the grant sample. Endpoint-excluding until permits same-edge readmission. Use a strong-until form when this property must also require grant eventually.

When valid is sampled high and ready low, require valid to remain high and payload to remain stable on the next sampled clock. Repeating this one-step invariant on every stalled edge naturally holds the transaction until acceptance.

Treat valid && !ready as the stall condition. If it is true for five consecutive sampled clocks, require it to be false on the next sample. A shorter stall never completes the five-cycle antecedent, so it creates no failure.

If request remains asserted through grant, gnt |-> req is enough. If request is a pulse and grant may arrive later, track outstanding state or check a bounded request history. The property must match the protocol's ownership model.

A property-local variable can capture a request tag separately for every attempt and require a later matching response. That proves value correlation for each attempt, but it does not consume a response. Reused tags or overlapping attempts can let one response satisfy several obligations, so one-to-one and FIFO order need explicit state or a scoreboard.