Spec to Verification Plan

Feature extraction — read the spec like a verifier

A verification plan starts with a feature list : every behavior the spec promises, written as a verifiable statement. Read the spec three times — once for understanding, once extracting every "shall/must/will" into a feature row, and once hunting for what the spec does not say (undefined behavior, missing corner cases, implicit assumptions). The third pass finds the most bugs.

FEATURE EXTRACTION PASSES

  Pass 1: Understand     "What does this block do?"
  Pass 2: Extract        Every shall/must/will → one feature row
                         "FIFO shall assert full when count == DEPTH"
                         "Write to full FIFO shall be ignored"
  Pass 3: Interrogate    What is NOT specified?
                         "What happens on simultaneous push+pop at full?"
                         "Is read data valid the same cycle as pop?"
                         → spec ambiguity log, NOT a guess

Good vs bad feature rows

• Good: "On reset assertion mid-burst, FIFO flags return to empty within 1 cycle" — specific, observable, checkable.

• Bad: "FIFO works correctly" — not verifiable, not closeable, hides ten real features.

• Good: "Back-to-back writes at full rate for DEPTH+2 cycles trigger full exactly once" — defines the stimulus and the check.

• Each row maps to exactly one check and one or more coverage points — if you cannot name the check, the row is not done being written.

Risk ranking — verify the scary things first

Not all features deserve equal effort. Rank by bug likelihood × bug cost . New logic, clock-domain crossings, arbitration, and anything with state ranks high. A pass-through register bank ranks low. Risk ranking decides what gets constrained-random plus formal versus a single directed test.

RISK MATRIX

                       Bug cost (silicon respin / field failure)
                       LOW                    HIGH
  Bug          LOW  │  directed test,      │  directed + assertions
  likelihood        │  low priority        │  (cheap insurance)
               ─────┼──────────────────────┼─────────────────────────
               HIGH │  constrained-random  │  random + formal + 
                    │  + coverage          │  dedicated owner + 
                    │                      │  first on schedule

  High-likelihood signals: new logic, CDC, arbitration, deep FSMs,
  corner-heavy datapaths, anything the designer says "should be fine"

Plan structure — feature / approach / coverage / owner

Every plan row carries four mandatory columns. The discipline matters more than the tool — a spreadsheet works fine if every row is honest.

VERIFICATION PLAN STRUCTURE

  ID    │ Feature              │ Approach          │ Coverage / Check     │ Owner │ Status
  ──────┼──────────────────────┼───────────────────┼──────────────────────┼───────┼───────
  F-001 │ full asserts at      │ random + directed │ cp_count.full bin,   │ SB    │ open
        │ count == DEPTH       │ boundary test     │ a_full_when_count    │       │
  F-002 │ write @ full ignored │ assertion + error │ a_no_push_full,      │ SB    │ open
        │                      │ injection test    │ x_full_write cross   │       │
  F-003 │ reset mid-traffic    │ directed reset    │ cp_reset_during_     │ RK    │ open
        │ returns to empty     │ storm test        │ traffic bin          │       │
  F-004 │ data integrity,      │ scoreboard,       │ scoreboard compare   │ SB    │ open
        │ in-order             │ all tests         │ count > 10k          │       │

  Rules:
  - Approach names the methodology, not "test it"
  - Coverage column names the bin/assertion — traceable to closure report
  - Owner is a person, not a team
  - Status is open / coded / passing / closed (closed = coverage hit + check active)

Spec-ambiguity logging

Every question Pass 3 raises goes into an ambiguity log with the question, the date, who must answer (architect or designer), and the answer once given. Never resolve an ambiguity by reading the RTL — the RTL is the thing under test, and matching it makes your checker a tautology. The log is a deliverable: at plan review, open ambiguities are schedule risks.

• Log entry: "Q-007: simultaneous push+pop at full — accept push? Asked arch 03-12. Answer 03-14: pop wins, push ignored, spec v1.3 updated."

• An answered ambiguity becomes a new feature row — Q-007 becomes F-015 with its own check.

• Unanswered ambiguities at sign-off are documented as verification holes, not silently dropped.

Plan review gates

The plan is reviewed at minimum twice : once before testbench coding starts (does the plan cover the spec? are approaches right-sized?) and once before sign-off (is every row closed or explicitly waived?). Reviewers must include the designer — they know where the bodies are buried — and ideally an engineer from outside the block.

1. Gate 1 — plan review: feature list vs spec walk-through, risk ranking challenge, ambiguity log triage. Exit: plan baselined.

2. Gate 2 — mid-point health check (optional but wise): rows closed vs schedule, new features from spec changes folded in.

3. Gate 3 — sign-off review: every row closed/waived with evidence, coverage report attached, open bugs dispositioned.

Key takeaways

• Three spec passes: understand, extract shall/must rows, interrogate the gaps.

• Risk-rank features — effort follows bug likelihood × bug cost.

• Every plan row: feature, approach, coverage/check name, owner, status.

• Ambiguities go to the architect in a log — never resolved by reading RTL.

Common pitfalls

• Vague feature rows ("FIFO works") — unclosable and hide real features.

• Resolving spec gaps from RTL — checker becomes a tautology that passes by construction.

• Plan written once and never updated — by sign-off it describes a different project.

• Skipping designer participation in plan review — they know the risky logic you cannot see.