assert, assume, cover, restrict & Action Blocks

Four verbs for one property

The verification directive is the top layer of SVA: it takes a property and tells the tool what to do with it. The same property text can be checked (assert), used as an input constraint (assume), counted as a scenario (cover), or used to prune the formal state space (restrict). Crucially, the four verbs mean different things to a simulator and a formal tool — knowing both columns of that table is what the interview question is really asking.

DIRECTIVE SEMANTICS — simulation vs formal

  ┌──────────┬──────────────────────────────┬──────────────────────────────┐
  │ directive│ SIMULATION                   │ FORMAL                       │
  ├──────────┼──────────────────────────────┼──────────────────────────────┤
  │ assert   │ check; report failure        │ obligation: PROVE it holds   │
  │          │ when property is violated    │ for ALL legal input traces   │
  ├──────────┼──────────────────────────────┼──────────────────────────────┤
  │ assume   │ checked exactly like assert  │ constraint: tool only        │
  │          │ (verifies your TB obeys it)  │ explores traces where it     │
  │          │                              │ holds (defines "legal")      │
  ├──────────┼──────────────────────────────┼──────────────────────────────┤
  │ cover    │ count matches; never errors  │ reachability: find a trace   │
  │          │ (scenario was exercised)     │ that satisfies it (witness)  │
  ├──────────┼──────────────────────────────┼──────────────────────────────┤
  │ restrict │ IGNORED entirely             │ constraint like assume, but  │
  │          │ (no checking, no cost)       │ with no simulation checking  │
  └──────────┴──────────────────────────────┴──────────────────────────────┘

  assume vs restrict in one line: both constrain formal; simulation
  CHECKS assume but IGNORES restrict. Use restrict for case-splitting
  (e.g. pin mode select) that simulation should not be forced to obey.

// One interface, all four verbs doing their natural jobs
// 1. assert — the DUT obligation
ap_no_overflow: assert property (@(posedge clk) disable iff (!rst_n)
  !(push && full)) else $error("FIFO pushed while full");

// 2. assume — environment contract (formal constraint, sim-checked)
am_pop_legal: assume property (@(posedge clk) disable iff (!rst_n)
  !(pop && empty));

// 3. cover — prove the interesting scenario actually happens
cp_full_hit: cover property (@(posedge clk) disable iff (!rst_n)
  full ##1 !full);

// 4. restrict — formal case split; simulation ignores it
rs_mode: restrict property (@(posedge clk) mode == 2'b01);

Action blocks

An assert (or assume) directive takes an optional action block : a pass statement, an else fail statement, or both. Action blocks are procedural code executed in the Reactive region after the attempt completes — so they may call tasks, increment counters, or dump state, not just print. The fail action is where 99% of real usage lives; pass actions are for debug bring-up only (they execute on every non-vacuous pass — on a hot assertion that is a firehose).

int unsigned err_count;

ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
  req |-> ##[1:3] ack)
  // pass action (rarely used — noisy):
  // $info("ap_req_ack pass at %0t", $time);
  else begin
    err_count++;
    $error("[%0t] ap_req_ack: req at %0t got no ack in 3 cycles (err #%0d)",
           $time, $time - 3*CLK_PERIOD, err_count);
    if (err_count > 10) $fatal(1, "too many handshake errors, aborting");
  end

• Action blocks run with CURRENT values in the Reactive region — signals may have moved on since the sampled values that decided the attempt; print sampled values via $sampled(sig) if exactness matters.

• Default fail action (no else) is an implicit $error with a tool-generated message — functional, but the label is then your only triage handle.

• Fail actions of windowed properties run at window END; compute the attempt start time in the message (as above) to point debuggers at the cause.

• In UVM environments, call uvm_report routines from the action block (or use the SVA-to-UVM report catcher glue) so assertion failures share the report server's counting and demotion machinery.

Severity system tasks

Inside action blocks (and immediate assertions), four severity tasks classify the event: $info, $warning, $error, and $fatal. They differ in the message tag, the effect on simulation, and how regression scripts count them. $error is the default severity of a failing assertion with no action block.

SEVERITY LADDER

  $info     informational     sim continues   never fails a regression
  $warning  suspicious        sim continues   counted; usually non-fatal
  $error    check failed      sim continues   fails the test in scripts
  $fatal    unrecoverable     $finish called  immediate stop
            ($fatal(status) — first arg is the exit status code)

  Choosing severity = answering "what should a nightly regression do?"
    protocol rule broken          → $error  (let sim run; gather more)
    x/z on control in active use  → $error or $fatal per project policy
    clock stopped / TB integrity  → $fatal  (everything after is noise)
    perf hint (almost-full often) → $warning or $info

// Severity choices in practice
ap_proto: assert property (@(posedge clk) disable iff (!rst_n)
  valid |-> !$isunknown(data))
  else $error("X on data while valid");          // keep simulating

ap_clk_alive: assert property (@(posedge ref_clk)
  ##[1:100] $changed(core_clk))
  else $fatal(1, "core_clk stopped — aborting"); // nothing else matters

cp_near_full: cover property (@(posedge clk) fifo_cnt >= DEPTH-2);
// covers have no action block in most styles — count is the product

Labels and naming conventions

The identifier before the colon — ap_req_ack: — is the assertion label . It appears in failure messages, assertion-coverage reports, waveform assertion panes, and tool on/off controls ($assertoff with hierarchical names). An unlabeled assertion is reported by file/line — useless once the file moves. Treat labels as API: stable, greppable, and encoding the directive type.

// A common convention: prefix encodes the directive
//   ap_  assert property      am_  assume property
//   cp_  cover property       rs_  restrict property
//   a_   immediate assert
// then <block>_<rule>:
ap_axi_aw_handshake : assert property (p_handshake(awvalid, awready, 16));
ap_fifo_no_overflow : assert property (p_no_overflow);
cp_fifo_wrap        : cover  property (p_wrap_around);
am_axi_master_legal : assume property (p_master_obligations);

// Labels enable surgical sim control:
initial begin
  $assertoff(0, top.dut_wrap.ap_fifo_no_overflow);  // during error injection
  // ... injection scenario ...
  $asserton (0, top.dut_wrap.ap_fifo_no_overflow);
end

Why labels matter operationally

• Regression triage greps the label — ap_fifo_no_overflow groups a thousand failures into one bug, file:line does not.

• Assertion coverage reports are keyed by label — naming by rule makes the report read like the verification plan.

• Tool controls ($assertoff/$asserton/$assertkill) address assertions by hierarchical label path.

• Stable labels survive refactors; auto-generated names break every diff-based dashboard.

Interview angle

The high-yield question here is the assume/assert/restrict triangle: "What does assume do in simulation?" Model answer: in simulation, assume is checked exactly like assert (it verifies your stimulus honors the environment contract); in formal, it constrains the input space the prover explores. restrict constrains formal the same way but is completely ignored in simulation. Candidates who answer only the formal half are flagged as never having run their assumptions in a simulator.

• Trap question: "A formal proof passed but the same RTL fails in simulation — how?" — over-constraining: an assume (or restrict) excluded the trace simulation generated; assumptions define 'legal' and wrong assumptions hide real bugs.

• Trap question: "What does a failing cover mean?" — covers do not fail; a never-hit cover means the scenario was never exercised (sim) or is unreachable (formal) — a stimulus or constraint problem, not a DUT bug.

• Trap question: "When do action-block prints show stale values?" — action runs in the Reactive region with current values; the deciding values were the sampled ones; use $sampled() for faithful prints.

• Follow-up: "How do you turn assertions off during error injection?" — $assertoff on labeled paths, or a TB-controlled disable iff term; mention re-enabling and the risk of forgetting.

Key takeaways

• assert checks, assume constrains formal (but is CHECKED in simulation), cover measures, restrict constrains formal only.

• Action blocks are full procedural code in the Reactive region; fail actions carry the triage payload — include the attempt start time.

• Severity = regression policy: $error keeps gathering data, $fatal stops a meaningless simulation.

• Label every directive with a stable, convention-bearing name — labels are the API for triage, coverage, and tool control.

• Vacuously passing asserts and never-hit covers are the same disease: the interesting scenario never happened.

Common pitfalls

• Believing assume is ignored in simulation — it is checked; a violated assumption fails the sim run.

• Over-constraining formal with convenience assumes — the proof becomes 'holds for inputs that never happen'.

• Pass action blocks left on in regression — log explosion on every non-vacuous pass of a hot assertion.

• $fatal for recoverable protocol slips — one minor error kills a 6-hour run and all the data after it.

• Unlabeled assertions — failures keyed by file:line break every grep, dashboard, and $assertoff control the moment the file is edited.