Challenge the implementation.
Part 3 · Proof and reset
SystemVerilog AssertionsReset, vacuity, and meaningful proof
Control property lifetime, expose unreachable success, and separate implementation checks, environment assumptions, and reachability evidence.
Question directory
Questions for Proof + reset
Open a question at its supporting explanation. The complete property reference stays directly above each answer set.
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?→
05 · Reset and meaningful proofMake 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.
Concept modelAssert, assume, and cover answer different questions
Define a legal environment.
Demonstrate reachability.
Meaningful proofchecker + honest assumptions + reachable scenario
Always-visible reference
Learn the mechanism before testing the interview answer.
These notes, tables, examples, and design limits contain the working knowledge for this chapter. The interview questions below are a checkpoint, not the primary explanation.
Attempt lifetime
Abort, accept, reject, and block are different outcomes.
Choose the control that matches the specification. Reset commonly discards an in-flight attempt; a flush may explicitly accept or reject it; expect waits procedurally for completion.
| Construct | Condition observation | Effect on active attempt | Typical use |
|---|---|---|---|
disable iff (x) | Asynchronous current value | Abort with no pass or failure | Reset invalidates transaction |
accept_on (x) | Asynchronous current value | Terminate as success | External event makes obligation acceptable |
reject_on (x) | Asynchronous current value | Terminate as failure | External event makes obligation invalid |
sync_accept_on (x) | Sampled on property clock | Terminate as success | Clocked acceptance policy |
sync_reject_on (x) | Sampled on property clock | Terminate as failure | Clocked rejection policy |
expect (property) | Property sampling semantics | Block process until success or failure | Procedural test scenario |
Reset release
Reset abort and post-reset startup are two separate contracts.
disable iff controls whether attempts exist while reset is active. A second property should describe what is legal on and after deassertion.
- Use |=> when the first protected sample is after the release edge.
- Use |-> only when the release edge itself is part of the protected interval.
- A sampled high reset level is not a release event. Use $rose(rst_n) for active-low reset deassertion.
- Synchronize asynchronous reset release when the design contract requires a clean first active clock.
Three quiet samples after releaseSystemVerilog
a_quiet_after_reset: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(rst_n) |=>
(!enable && !data_valid)[*3]
);
Verification roles
Assert, assume, cover, and coverage reports answer different questions.
A proof is meaningful only when the checker is correct, the environment assumptions are honest, and the interesting behavior is reachable.
| Mechanism | Question | What it proves | What it does not prove |
|---|---|---|---|
assert property | Must this always hold? | No allowed trace violates the property in the analysis scope | The property fully represents the specification |
assume property | What may the environment do? | Only assumed-legal traces are explored in formal | The environment will drive that behavior in simulation |
cover property | Can this temporal scenario occur? | At least one trace reaches the scenario | All safety behavior is correct |
assertion coverage | Was the checker exercised? | Attempts, outcomes, and possible vacuity data | Value-space completeness |
covergroup | Which values and crosses occurred? | Bins and sampled combinations | A multi-cycle protocol path |
Meaningful proof
Treat a formal PASS as the end of an audit, not the start of a celebration.
Formal analysis explores all traces allowed by the model and assumptions. The result is only as useful as the proof boundary, clocks, resets, X semantics, fairness, and reachability evidence.
Correct obligation
Review sampled edges, antecedent triggers, endpoints, and overlapping attempts against the written requirement.
Honest assumptions
Assume only behavior guaranteed by the real integration. Prove or review every assumption source.
Useful cover traces
Cover reset release, triggers, earliest and latest legal responses, and states needed to exercise the checker.
Completion policy
Prefer finite deadlines. Justify every unbounded eventuality and fairness assumption in plain language.
Cover trigger, completion, and boundarySystemVerilog
c_request_seen: cover property (
@(posedge clk) disable iff (!rst_n)
$rose(req)
);
c_latest_legal_ack: cover property (
@(posedge clk) disable iff (!rst_n)
$rose(req) ##3 $rose(ack)
);
c_state_path: cover property (
@(posedge clk) disable iff (!rst_n)
state == S0 ##1 state == S1
##1 state == S2
##1 state == S3
);
Diagnostics
Action blocks control regression response, not property truth.
The property already passed or failed before its action block runs. Choose severity to match the verification policy and report sampled context that makes the failure reproducible.
| Task | Typical policy | Simulation effect |
|---|---|---|
$fatal | Cannot continue meaningfully | Report and terminate |
$error | Regression failure | Report error; simulator normally continues |
$warning | Suspicious but tolerated condition | Report warning |
$info | Diagnostic or progress message | Report information |
Pass and fail action blocksSystemVerilog
a_packet_length: assert property (
@(posedge clk) disable iff (!rst_n)
sop |-> length inside {[1:MAX_LEN]}
) begin
packet_checks_passed++;
end else begin
$error(
"bad length=%0d at packet start",
$sampled(length)
);
end
Interview checkpoint
Explain the rule, then defend its edge cases.
Open a prompt after studying the reference above. A strong answer should name the sampled edge, match endpoint, failure mode, and proof evidence.
Strong answer
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.
Why it works
- It is an attempt-lifetime control, not merely an antecedent that happens to mention reset.
- If reset asserts while a request-to-response attempt is pending, that attempt is terminated unless the specification says reset must preserve it.
- Reset release semantics still need a design contract. A synchronously released reset can avoid ambiguous first-cycle behavior in the design and its assertions.
What the interviewer is testing
Whether you distinguish asynchronous abort from a synchronously sampled reset condition.
Common trap
Do not claim disable iff pauses an attempt and resumes it after reset.
Abort active attempts during resetSystemVerilog
a_req_ack: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |-> ##[1:3] ack
);
Strong answer
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.
Why it works
- $rose(rst_n) |=> (!enable && !data_valid)[*3] protects the first three samples after the release edge.
- Keep disable iff (!rst_n) so attempts are aborted while reset is active, but do not assume it defines the post-reset startup contract.
- Decide whether the release edge itself counts. Choosing |-> instead of |=> moves the first protected sample onto that edge.
What the interviewer is testing
Whether you separate reset abort behavior from the temporal contract that begins when reset is released.
Common trap
A reset disable clause alone does not guarantee any settling or idle cycles after deassertion.
Hold startup traffic quiet for three clocksSystemVerilog
a_quiet_after_reset: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(rst_n) |=>
(!enable && !data_valid)[*3]
);
Strong answer
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.
Why it works
- At a formal block boundary, assume only behavior guaranteed by the real environment. Overconstraint can make a false design look proven.
- Use cover to test reachability and to find example traces for useful boundary scenarios.
- A clean simulation regression is evidence about those finite tests, not an exhaustive proof over all legal inputs and states.
- cover property measures a temporal scenario; it complements but does not replace covergroups, cross coverage, or the tool's assertion attempt/pass/fail coverage.
What the interviewer is testing
Whether you can define the proof boundary and audit assumptions rather than treating a formal PASS badge as self-explanatory.
Common trap
Never turn an implementation obligation into an assumption simply to make the proof converge.
| Directive | Question answered | Main risk |
|---|---|---|
assert property | Must this always hold? | Wrong or incomplete property |
assume property | What may the environment do? | Overconstraint |
cover property | Can this scenario occur? | Confusing reachability with correctness |
Strong answer
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.
Why it works
- Cover an implication antecedent separately when you need evidence that a passing checker was actually activated.
- Use temporal cover properties for protocol paths and latency boundaries, such as earliest and latest legal responses.
- Use covergroups when the requirement is about value combinations, distributions, or crosses rather than one temporal path.
What the interviewer is testing
Whether you can build a coverage plan that distinguishes a reachable behavior from a well-exercised checker and from value-space coverage.
Common trap
A cover property hit proves that one scenario occurred; it does not prove the associated safety requirement is correct on every trace.
Cover trigger and boundary latencySystemVerilog
c_request_seen: cover property (
@(posedge clk) disable iff (!rst_n)
$rose(req)
);
c_latest_legal_ack: cover property (
@(posedge clk) disable iff (!rst_n)
$rose(req) ##3 ack
);
Strong answer
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.
Why it works
- Prefer a finite deadline when the architecture defines one. It is easier to debug and usually easier to prove.
- Use strong around an eventual sequence when an unfinished end-of-simulation attempt must count as failure.
- State every fairness assumption in plain language and prove that the real environment actually supplies it.
What the interviewer is testing
Whether you separate bounded safety checks from genuine liveness and understand why time horizon and environment fairness affect the result.
Common trap
Adding strong does not create a realistic deadline, and adding fairness does not repair an environment that can legally stall forever.
Require an eventual bounded match to completeSystemVerilog
a_req_ack_bounded: assert property (
@(posedge clk) disable iff (!rst_n)
$rose(req) |->
strong(1'b1 ##[1:5] ack)
);
Strong answer
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.
Why it works
- Use disable iff for reset-style invalidation, when an interrupted transaction should not be counted as either correct or incorrect.
- Use accept_on or reject_on only when the specification explicitly assigns a success or failure outcome to an external abort condition such as a flush.
- Because asynchronous controls observe current values, choose the sync form when the contract requires a sampled decision.
What the interviewer is testing
Whether you distinguish discarding an attempt from deliberately completing it with a result, and whether you know that expect has procedural blocking behavior.
Common trap
Do not replace reset disable with accept_on just because both stop evaluation; one discards the attempt and the other declares success.
Treat flush as an accepted terminationSystemVerilog
a_req_ack_or_flush: assert property (
@(posedge clk) disable iff (!rst_n)
accept_on (flush)
($rose(req) |-> ##[1:3] ack)
);