Protocol Assertion Cookbook

Overview

Everything before this point — sequences, implication, repetition, sampled value functions — exists so you can write the contents of this topic: complete, deployable rulesets for the interfaces every chip actually has. Real protocol checking is never one assertion. A valid/ready interface needs stability rules, X rules, and a liveness rule together; a FIFO needs occupancy math, flag exclusivity, and data integrity together. One missing rule and the checker passes while the bus burns.

This is also the most interview-loaded topic in all of SVA. “Write the assertions for an AXI-style handshake” or “what would you assert on a FIFO?” are the standard whiteboard prompts for verification roles, and the grading rubric is completeness: interviewers count how many of the canonical rules you produce unprompted, and whether you can defend each one with a waveform. Each sub-lesson below is structured as that answer — the full ruleset, the waveforms, and the reasoning.

Sub-topics

1. Valid/Ready Handshake Assertions — the full AXI-style ruleset: stability, X-safety, liveness, dependency rules.

2. Request/Acknowledge Protocols — hold-until-ack, bounded ack windows, pulse discipline, spacing rules.

3. FIFO Assertions — push/pop legality, occupancy consistency, flag exclusivity, data integrity, async notes.

4. FSM Assertions — one-hot encoding, legal-transition tables, bounded deadlock checks, reset state, cover points.

5. Stability, Pulse & Glitch Checks — throughout, exact pulse widths, mutual exclusion, interrupt persistence.

6. Pipeline & Datapath Assertions — fixed-latency equality, stall correctness, in-order completion, credit counters.

PROTOCOL ASSERTION COOKBOOK — TOPIC MAP

                        ┌─────────────────────────┐
                        │  interface under check  │
                        └────────────┬────────────┘
            ┌────────────────┬───────┴───────┬────────────────┐
            ▼                ▼               ▼                ▼
     ┌────────────┐   ┌────────────┐  ┌────────────┐   ┌────────────┐
     │ handshake  │   │  storage   │  │  control   │   │  datapath  │
     │            │   │            │  │            │   │            │
     │ valid/ready│   │   FIFO     │  │   FSM      │   │ pipelines  │
     │ req/ack    │   │ occupancy  │  │ transitions│   │ latency    │
     └─────┬──────┘   └─────┬──────┘  └─────┬──────┘   └─────┬──────┘
           │                │               │                │
           ▼                ▼               ▼                ▼
     stability +      count math +    legal arcs +     out==$past(in)+
     X-safety +       flag exclus. +  no deadlock +    stall holds +
     liveness         data integrity reset + covers   credits bounded
           │                │               │                │
           └────────────────┴───────┬───────┴────────────────┘
                                    ▼
                    every ruleset = SAFETY rules ("never bad")
                                  + LIVENESS rules ("eventually good")
                                  + X rules      ("payload known")
                                  + COVER points ("we exercised it")

Key takeaways

• Protocol checking means rulesets, not single assertions — completeness is the quality metric.

• Every ruleset mixes safety, bounded liveness, X-safety, and cover points.

• These six interface families cover the overwhelming majority of real-world assertion work.

• Interview prompts grade you on how many canonical rules you produce unprompted — learn them as sets.