Part 4 · Assertions (SVA) · Intermediate

SystemVerilog Assertions — Interview-Critical Deep Dive

Concurrent assertions from boolean layer to formal-ready properties: sequences, implication, sampled value functions, protocol checkers, debug, and dedicated interview drill modules.

What assertions buy you

A scoreboard tells you that something went wrong, often thousands of cycles after the corruption happened. An assertion tells you where and when — it fires on the exact clock edge the protocol rule was violated, at the exact signal that broke it. That bug time-locality is the single biggest practical win of SVA: debug time collapses from hours of waveform archaeology to reading one failure message.

Assertions are also specification as code . A written spec says "req must be held until ack"; an assertion makes that rule executable, checked on every cycle of every test, forever. And the same property text is reusable by formal verification tools, which exhaustively prove it over all input sequences instead of just the ones your tests happened to generate. One artifact, three payoffs: simulation checking, living documentation, formal proof.

Topic map

diagram
Legend: [CORE] [TEMPORAL] [APPLIED] [INTERVIEW]

┌──────────────────────────────────────────────────────────────────────────┐
│  SVA SECTION — topic map                                                  │
├──────────────────────────────────────────────────────────────────────────┤
│                                                                           │
│  1. SVA FUNDAMENTALS [CORE]                                               │
│     immediate vs concurrent │ 4 layers │ sampling │ attempts │ reset      │
│                                                                           │
│  2. SEQUENCES [TEMPORAL]                                                  │
│     ##delay │ repetition [*] [=] [->] │ and/or/intersect │ throughout     │
│                                                                           │
│  3. IMPLICATION & PROPERTIES [TEMPORAL]                                   │
│     |-> vs |=> │ vacuity │ until/s_until │ eventually │ nested props      │
│                                                                           │
│  4. SAMPLED VALUE FUNCTIONS [CORE]                                        │
│     $rose $fell $stable $changed │ $past │ $countones $onehot             │
│                                                                           │
│  5. PROTOCOL ASSERTIONS [APPLIED]                                         │
│     req/ack │ handshakes │ FIFO │ arbiter │ bus rules │ checker modules   │
│                                                                           │
│  6. ADVANCED SVA [TEMPORAL]                                               │
│     local variables │ multiclock │ recursion │ expect │ bind              │
│                                                                           │
│  7. ASSERTION DEBUG [APPLIED]                                             │
│     vacuous passes │ thread viewing │ severity │ coverage of assertions   │
│                                                                           │
│  8. INTERVIEW SVA PATTERNS [INTERVIEW]  ◄── drill module                  │
│     the 15 assertions every interview asks │ write-it-live practice       │
│                                                                           │
│  9. INTERVIEW Q&A [INTERVIEW]           ◄── drill module                  │
│     rapid-fire concept questions │ trap questions │ whiteboard prompts    │
│                                                                           │
└──────────────────────────────────────────────────────────────────────────┘

Topics in this section

  1. SVA Fundamentals — immediate vs concurrent, the four layers, preponed sampling, evaluation attempts, disable iff, directives.

  2. Sequences — cycle delays, repetition operators, sequence composition, throughout/within.

  3. Implication & Properties — |-> and |=>, vacuity, property operators, strong vs weak.

  4. Sampled Value Functions — $rose/$fell/$stable/$past and friends, with exact sampling semantics.

  5. Protocol Assertions — real handshake, FIFO, and arbiter checkers built rule by rule.

  6. Advanced SVA — local variables, multiclock properties, bind, recursive properties.

  7. Assertion Debug — vacuity analysis, thread debugging, assertion coverage.

  8. Interview SVA Patterns — the canonical write-this-assertion prompts, solved and dissected.

  9. Interview Q&A — rapid-fire concept and trap questions with model answers.


Anatomy of a concurrent assertion

Every concurrent assertion is built from four layers, each one consuming the layer below it. Internalize this picture — most SVA confusion comes from mixing up which layer an operator belongs to.

diagram
ANATOMY — from directive down to booleans

  ap_req_ack: assert property (p_req_ack)        ◄── LAYER 4: VERIFICATION DIRECTIVE
              else $error("req/ack broke");          assert / assume / cover / restrict
       │                                             label + action block
       ▼
  property p_req_ack;                            ◄── LAYER 3: PROPERTY
    @(posedge clk) disable iff (!rst_n)              clock, reset gating,
    req |-> s_ack_window;                            implication, property operators
  endproperty
       │
       ▼
  sequence s_ack_window;                         ◄── LAYER 2: SEQUENCE
    ##[1:3] ack;                                     temporal shape: delays,
  endsequence                                        repetition, composition
       │
       ▼
  req, ack, !rst_n                               ◄── LAYER 1: BOOLEAN
                                                     plain expressions over
                                                     sampled signal values

  Rule of thumb:
    booleans    ARE things true now?
    sequences   in what ORDER over which CYCLES?
    properties  what is REQUIRED to follow from what?
    directives  what should the TOOL do about it?

Interview drill modules

Topics 8 and 9 are interview drill modules , not theory. Topic 8 walks through the assertion-writing prompts that appear in nearly every verification interview (req/ack windows, stability rules, one-hot checks, FIFO invariants) with cycle-accurate solutions. Topic 9 is rapid-fire concept questions — sampling regions, vacuity, |-> vs |=> — phrased the way interviewers actually ask them. Do topics 1–7 first; drill 8–9 until you can produce the answers cold.

Key takeaways

  • Assertions localize bugs in time — failure fires at the violating clock edge, not test end.

  • One property serves three masters: simulation checking, executable spec, formal proof.

  • The four-layer model (boolean → sequence → property → directive) organizes every SVA construct.

  • Topics 8–9 are interview drills — SVA is one of the two most heavily probed interview areas.

Common pitfalls

  • Treating SVA as syntax memorization — interviews probe sampling semantics and attempt model, not keywords.

  • Writing assertions without understanding preponed sampling — waveform and assertion disagree, trust collapses.

  • Skipping vacuity analysis — a suite of passing assertions may be checking nothing at all.

  • Putting temporal protocol checks in scoreboards — cycle-level rules belong in assertions, transaction-level in scoreboards.