SVA Fundamentals

Overview

Everything else in SVA — sequences, implication, protocol checkers — sits on the foundations in this topic. Before any temporal operator makes sense you must know when signals are sampled (preponed region, values from before the clock edge), and how attempts work (a fresh evaluation starts on every single clock tick, not once per test). These two facts explain nearly every "my assertion disagrees with the waveform" confusion — and they are the two facts interviewers probe first.

The topic also covers the structural basics: the split between assert statements inside procedural code (immediate) and clocked assert property (concurrent), the four-layer construction model, reset gating with disable iff, and what each verification directive actually instructs the tool to do.

Sub-topics

1. Immediate vs Concurrent Assertions — procedural instant checks vs clocked temporal properties, and where each belongs.

2. The Four Layers of SVA — boolean → sequence → property → directive, with named reuse and arguments.

3. Clocks & the Sampling Model — preponed-region sampling, the most misunderstood fact in SVA.

4. Evaluation Attempts & Threads — a new attempt every clock tick, overlapping attempts, thread spawning.

5. disable iff & Reset Handling — async abort semantics and reset gating patterns.

6. assert, assume, cover, restrict & Action Blocks — directive semantics in sim vs formal, severity tasks, labeling.

THE TWO FOUNDATION FACTS

  FACT 1 — PREPONED SAMPLING
  clk      _____/▔▔▔▔▔\_____/▔▔▔▔▔\_____
                ▲
                │ assertion evaluates HERE at the edge...
           sig ─┤
                └─ ...but uses the value sig had just BEFORE the edge
                   (preponed region, like a flip-flop's D input)

  FACT 2 — AN ATTEMPT EVERY TICK
  clk tick:   T0    T1    T2    T3    T4
  attempt A0  ●────────────►            a new, independent evaluation
  attempt A1        ●────────────►      of the property begins at
  attempt A2              ●──────►      EVERY clock tick
  attempt A3                    ●──►

How this topic is probed in interviews

• "Difference between immediate and concurrent assertions?" — warm-up question, expected in 30 seconds.

• "When is the signal sampled relative to the clock edge?" — the preponed-region question; most candidates get it wrong.

• "What happens to an assertion during reset?" — expects disable iff plus what happens to in-flight attempts.

• "What does assume do in simulation vs formal?" — separates candidates who have used formal from those who have not.

Key takeaways

• Concurrent assertions sample in the preponed region — values from before the clock edge.

• A new evaluation attempt starts at every clock tick; attempts overlap and are independent.

• Master the four-layer model before touching temporal operators — every construct lives in exactly one layer.

• disable iff is the standard reset gate; it asynchronously kills in-flight attempts.