Chapter 3 · Proof & reset

Reset, vacuity, and meaningful proof

Control property lifetime, expose unreachable success, and separate implementation checks, environment assumptions, and reachability evidence.

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

Watercolor of a verification workstation with waveform traces and a development board. — Turn timing contracts into checks.

The language bench / assertions

Give the response a deadline.

Sampled clock 0RESET RELEASED

Sampled values by clock cycle
Cycle	req	ack	reset
0	0	0	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

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?

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

Must holdassert

Challenge the implementation.

May occurassume

Define a legal environment.

Can occurcover

Demonstrate reachability.

Meaningful proofchecker + honest assumptions + reachable scenario

A checker constrains the implementation, an assumption constrains the modeled environment, and coverage proves that an interesting path is reachable.

Reference, examples and proof details

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.

Property

Correct obligation

Review sampled edges, antecedent triggers, endpoints, and overlapping attempts against the written requirement.

Environment

Honest assumptions

Assume only behavior guaranteed by the real integration. Prove or review every assumption source.

Reachability

Useful cover traces

Cover reset release, triggers, earliest and latest legal responses, and states needed to exercise the checker.

Liveness

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
);

disable iff
reset
abort
attempt

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]
);

reset release
$rose
[*3]
startup

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

assert
assume
cover
formal

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
);

cover property
assertion coverage
covergroup
vacuity

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
liveness
fairness
formal

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)
);

accept_on
reject_on
sync_accept_on
expect

Sampled values by clock cycle

Cycle

req

ack

reset

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

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

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 );

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

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