Clocks & the Sampling Model

The single most misunderstood fact in SVA

Concurrent assertions do not see the values your waveform viewer shows at the clock edge. They see the values signals held just before the edge — sampled in the preponed region , the very first region of the time slot, before any design logic has reacted to the clock. The mental model: an assertion samples a signal exactly the way a flip-flop samples its D input. If a signal changes at the same simulation time as the clock edge (as the output of every synchronous register does), the assertion uses the old value at that edge — and sees the new value only at the next edge.

PREPONED SAMPLING — sampled value vs displayed value

  clk        ____/▔▔▔▔\____/▔▔▔▔\____/▔▔▔▔\____
                 T1         T2         T3
  sig (sim)  0000│1111111111111111111111111111     ← sig driven to 1 AT T1
                 ▲          ▲          ▲             (nonblocking, edge-aligned)
  sampled    ────0──────────1──────────1───
  at edge:      T1: 0      T2: 1      T3: 1
                 │
                 └── waveform SHOWS 1 at T1, assertion SEES 0 at T1

  Why: the preponed region snapshots signals BEFORE the NBA updates
  triggered by this same edge take effect. Identical to what a
  flip-flop clocked at T1 would capture on its D pin.

This is why the sampling model exists at all: it makes assertion evaluation deterministic and race-free . If assertions read live values, their result would depend on whether the assertion process or the design's nonblocking updates ran first inside the time slot — a simulator-dependent race. Sampling before the edge removes the race and matches hardware register semantics exactly.

A worked trace: where waveform and assertion disagree

// DUT fragment: gnt is registered, one cycle after req
always_ff @(posedge clk) gnt <= req;

// Naive assertion: "whenever req, gnt is high one cycle later"
ap_gnt: assert property (@(posedge clk) req |-> ##1 gnt);

CYCLE-BY-CYCLE — why this PASSES even though it looks off-by-one

  clk          T0      T1      T2      T3
  req (sim)    0       1       0       0
  gnt (sim)    0       0       1       0      ← gnt <= req: rises at T2

  sampled req  0       1       0       0
  sampled gnt  0       0       1       0      ← at T2, gnt rose AT T2...
                                                 wait — preponed says OLD value?

  Careful: gnt is updated BY the T1 edge (NBA), so its new value 1 is
  stable throughout (T1,T2) and is ALREADY OLD by the time T2 samples.
  Preponed at T2 sees gnt = 1.   ✓

  attempt @T1: req=1 → check ##1 → @T2: gnt sampled 1 → PASS ✓

  The confusion case is signals changing exactly AT the sampling edge:
  at T1, sampled gnt is 0 (its pre-edge value), even though the viewer
  may draw the transition at T1. "Changed at the edge → assertion sees
  the old value at that edge, new value at the next."

The rule in one sentence

A concurrent assertion at edge N sees the values that were stable just before edge N — outputs of registers clocked by edge N-1, and combinational settles from the previous slot. Outputs produced by edge N itself become visible to the assertion at edge N+1.

Where the clock comes from

Every concurrent assertion needs a clocking event. It can be stated explicitly in the property, inherited from a default clocking block, or — for assertions embedded in clocked always blocks — inferred from the surrounding procedure. Explicit or default clocking are the styles to use; procedural inference is best treated as a curiosity that shows up in legacy code.

// 1. Explicit clock in the property — always unambiguous
ap_a: assert property (@(posedge clk) req |-> ##[1:3] ack);

// 2. Default clocking — declared once, inherited by clockless properties
default clocking cb @(posedge clk); endclocking

ap_b: assert property (req |-> ##[1:3] ack);          // uses cb's clock
ap_c: assert property (disable iff (!rst_n) !(push && full));  // ditto

// 3. Inferred from procedural context (legacy style — avoid)
always @(posedge clk)
  ap_d: assert property (req |-> ##1 gnt);            // clock inferred

// Multiple clocks — introduction (full treatment in Advanced SVA)
// A property may sequence across clock domains; each ## crossing
// re-synchronizes to the next edge of the NEW clock.
property p_cdc_handshake;
  @(posedge clk_a) req_a |=> @(posedge clk_b) ##[1:4] ack_b;
endproperty
ap_cdc: assert property (p_cdc_handshake)
  else $error("cross-domain ack missed window");

• default clocking removes per-assertion clock noise and keeps a file consistent — standard in checker files.

• An explicit @(...) in a property always overrides the default — handy for the odd negedge check in a posedge file.

• Multiclock sequencing uses the singly-clocked pieces joined by ##1/##[..]; the clock switch happens at the join (Advanced SVA covers the fine print).

Debugging a sampling disagreement

The standard triage when "the assertion is wrong"

1. Identify the exact failing edge from the assertion message (label + time).

2. For each signal in the property, ask: what was its value just BEFORE that edge? That is what the assertion used.

3. Check for edge-aligned transitions — signals that change at the failing edge are the usual suspects; the assertion saw their old value.

4. Check the waveform tool's delta/region view if available — many viewers can display preponed (sampled) values directly.

5. Only after the above, suspect the property logic itself.

TRIAGE PICTURE — "assertion failed but waveform looks fine"

  clk        ____/▔▔▔▔\____
                 Tf  ← failure reported here
  valid      ▁▁▁▁│▔▔▔▔▔▔▔▔   ← rises exactly AT Tf
                 ▲
  assertion sees valid = 0 at Tf  (pre-edge value)
  your eye sees   valid = 1 at Tf  (post-edge drawing)

  Neither is "wrong" — they are answers to different questions.
  The assertion's question matches what a flip-flop would capture.

Interview angle

"When does a concurrent assertion sample its signals?" is the question that separates candidates who have written assertions from those who have read about them. The model answer: in the preponed region of the time slot — values from just before the clock edge, exactly like a flip-flop's D input; a signal changing at the edge contributes its old value at that edge.

• Trap question: "My assertion fails but the waveform shows the signal high at that edge — tool bug?" — No; edge-aligned change, assertion correctly used the pre-edge value.

• Trap question: "Why not just sample current values?" — race with NBA updates; results would be simulator-order-dependent. Preponed sampling is what makes SVA deterministic.

• Follow-up: "How do you give a file of assertions one clock?" — default clocking; explicit @(...) overrides per property.

• Senior-level follow-up: relate it to regions — preponed (sample) → active/NBA (design) → observed (assertion evaluation) → reactive (action blocks/TB).

Key takeaways

• Assertions sample in the preponed region: pre-edge values, flip-flop semantics, race-free by construction.

• A signal changing at edge N is seen old at N and new at N+1 — the root of most waveform-vs-assertion confusion.

• Use default clocking for assertion files; explicit property clocks override it when needed.

• Evaluation uses sampled values but failure ACTION (the else block) runs later in the slot — message time equals edge time.

Common pitfalls

• Trusting the waveform's edge-aligned drawing over the sampled value — the assertion is right, your eye is wrong.

• Comparing assertion behavior against an immediate assert in always @(posedge clk) — the immediate one reads post-update values, results differ by one cycle.

• Forgetting default clocking exists in the file and double-clocking a property with a different edge by accident.

• Assuming $display inside an action block prints sampled values — it prints CURRENT values at action time, which may already differ.