Q&A: Assertion Fundamentals

Q: What is the difference between immediate and concurrent assertions?

Direct answer: an immediate assertion is a procedural statement — assert (expr) inside an always block, task, or function — evaluated instantly with the current (possibly mid-timestep) values, like an if-statement that errors. A concurrent assertion is declarative — assert property (@(posedge clk) ...) — evaluated on clock edges using values sampled in the Preponed region, and it can describe multi-cycle temporal behavior. Immediate = combinational check at a point in procedural code; concurrent = clocked temporal monitor that lives for the whole simulation.

// Immediate: procedural, instant, current values
always_comb begin
  if (sel) begin
    a_imm: assert (onehot_grant) else $error("grant not onehot");
  end
end

// Concurrent: declarative, clocked, sampled values, temporal
a_con: assert property (
  @(posedge clk) disable iff (!rst_n)
  $rose(req) |-> ##[1:4] ack);

Follow-up: 'Where can each be placed, and which kind races?'

Immediate assertions can sit anywhere procedural code runs — including classes and UVM components, which is why assert (obj.randomize()) is an immediate assertion. They are vulnerable to glitches and ordering races because they fire mid-timestep on whatever value happens to be there. Concurrent assertions only exist at module/interface/checker scope (or in procedural blocks as embedded concurrent assertions), and are race-free by construction because they read Preponed-sampled values.

Junior vs senior answer

• Junior: 'immediate is in always blocks, concurrent uses clocks' — true, stops at syntax.

• Senior: adds WHY it matters — sampling semantics (mid-timestep vs preponed), race exposure, temporal capability, and the randomize() connection that shows they have seen immediate asserts in real testbench code.

Q: When does a concurrent assertion sample its signals, and what does that imply?

Direct answer: in the Preponed region of the timestep containing the clock edge — i.e. the assertion sees the values signals held just before the clock edge, before any NBA updates from that edge. Consequence one: an assertion never sees the new value a flop takes on the same edge — it sees the old one. Consequence two: this is exactly the value a real flop would capture, so assertions behave like ideal registered checkers. Consequence three: the waveform viewer shows post-update values at the edge, so the viewer and the assertion routinely 'disagree' by one cycle — the assertion is not wrong.

Timestep at posedge clk (simplified region order):

  Preponed  ──► assertion SAMPLES here  (old values)
  Active    ──► blocking assigns, clk edge propagates
  NBA       ──► flops update            (new values)
  Observed  ──► assertion EVALUATES verdicts
  Reactive  ──► testbench reacts

  data flops from 0xAA to 0xBB at edge N:
    viewer cursor at edge N shows : 0xBB
    assertion at edge N samples   : 0xAA   ← one "cycle" apart

Follow-up: 'So when does the assertion verdict become visible?'

Evaluation happens in the Observed region of the same timestep, and action blocks run reactively — so a failure message prints in the timestep of the violating edge, but the values it reasoned about are the preponed ones. When debugging, shift your mental cursor one sample back from where the waveform cursor sits.

Junior vs senior answer

• Junior: 'it samples on the clock edge' — misses the before/after distinction that generates most assertion-debug confusion.

• Senior: names the region, states the flop analogy, and volunteers the waveform-disagreement consequence — pre-answering the most common debug question in the next lesson.

Q: What actually happens to a concurrent assertion on every clock edge?

Direct answer: the simulator starts a new evaluation attempt of the property at every sampling clock edge (outside disable iff). Each attempt independently evaluates the antecedent with that edge's sampled values; if the antecedent fails to match, the attempt ends as a vacuous success. If it matches, the attempt spawns the consequent obligation, which may run for many cycles — so at any moment, several attempts of the same assertion can be alive simultaneously, each tracking its own thread of the protocol.

a: assert property (@(posedge clk) $rose(req) |-> ##[1:4] ack);

cycle    :   0    1    2    3    4    5
req      :   0    1    0    1    0    0
ack      :   0    0    1    0    0    1

attempt@0: $rose(req)=0 → vacuous, done.
attempt@1: $rose(req)=1 → consequent thread waits, sees ack@2 ✓
attempt@2: vacuous.
attempt@3: $rose(req)=1 → second LIVE thread; sees ack@5 ✓
attempt@4,5: vacuous.

Two real threads coexisted (attempt@3 started while nothing
else pending). Overlapping traffic = overlapping attempts.

Follow-up: 'Why do I care about attempts in practice?'

• Performance: a level antecedent on a held signal multiplies live attempts — the retrigger storm anti-pattern.

• Reporting: each attempt passes/fails independently; one bad attempt among hundreds is a real failure, not noise.

• Local variables: each attempt gets a private copy — the reason tag-matching works and shared counting does not.

Junior vs senior answer

• Junior: 'it checks the property every clock' — hides the attempt/thread model entirely.

• Senior: attempts at every edge, vacuous early exit, concurrent live threads, and the three practical consequences (storms, per-attempt verdicts, per-attempt locals).

Q: assert vs assume vs cover — same property, three directives. What changes?

Direct answer: the obligation . assert property — the design must satisfy it; violations are failures. assume property — the environment is promised to satisfy it; in formal, the tool only explores stimulus where it holds (constraining the proof); in simulation, most tools check it like an assert (your testbench must honor its own promises). cover property — no obligation at all; it records whether the scenario ever occurred, measuring that your stimulus reached the behavior.

// One property, three roles around a DUT input 'req':
p_req_pulse: assert property (@(posedge clk) $rose(ack) |=> !ack);   // DUT duty
m_req_legal: assume property (@(posedge clk) $rose(req) |=> !req);   // env promise
c_b2b:       cover  property (@(posedge clk) req ##2 req);           // did we try it?

Follow-up: 'What happens if an assume is wrong in formal?'

Over-constraint: the tool prunes legal input behavior, the bad stimulus is never explored, and the assert 'proves' — a false proof. Worst case, contradictory assumes make EVERYTHING provable vacuously (no reachable states satisfy the assumptions). Senior habit: cover-check your assumes — write cover properties demonstrating that interesting stimulus still exists under the assumption set.

Junior vs senior answer

• Junior: 'assert checks, assume constrains, cover counts' — the table-row answer.

• Senior: adds the sim-vs-formal split for assume, the false-proof danger of over-constraint, and the cover-your-assumes discipline.

Q: Why do we label assertions?

Direct answer: the label (a_req_ack: assert property (...)) becomes the assertion's hierarchical name — and that name is the handle for everything downstream: log messages and triage scripts, waveform assertion tracks, per-assertion enable/disable ($assertoff and tool commands), formal result tables, and coverage/verification-plan mapping. Unlabeled assertions get tool-generated names like assert__42 that change when the file is edited — breaking scripts, waivers, and plan links silently.

// Naming convention carries the intent:
ap_axi_aw_stable:  assert property (p_aw_stable);   // ap_ = assert
cp_axi_b2b_write:  cover  property (p_b2b_write);   // cp_ = cover
mp_axi_no_x_in:    assume property (p_no_x_in);     // mp_ = assume
// label encodes: directive prefix + interface + behavior

Follow-up: 'Beyond the name — what else belongs on every assertion?'

• An action block with $error and a message naming the violated rule and key values — failure logs that read like the spec.

• A severity decision: $error for must-fix, $fatal for cannot-continue corruption, $warning for advisory checks.

• A matching cover (vacuity defense) and a comment or tag tying it to the spec clause it implements.

Junior vs senior answer

• Junior: 'so the log message is readable'.

• Senior: names the full consumer list — waivers, $assertoff control, formal tables, plan traceability — and the regression-breaking cost of auto-generated names drifting between edits.

Key takeaways

• Immediate = procedural and instant; concurrent = clocked, preponed-sampled, temporal — the sampling model is the real difference.

• A new attempt starts every clock; vacuous exits are normal, and live attempts overlap with traffic.

• assert/assume/cover share syntax and differ only in obligation — and a wrong assume in formal yields false proofs.

Common pitfalls

• Saying 'concurrent assertions see the waveform values' — they see preponed values, one sample earlier than the viewer cursor.

• Treating assume as documentation — in formal it actively removes stimulus; contradictions prove everything.

• Shipping unlabeled assertions — auto-names drift across edits and break waivers and triage scripts.