Verification Methodologies

Verification Foundations · Module 1 · Page 1.5

The Engineering Problem

The previous lesson named the obstacles — controllability, observability, reproducibility, concurrency, completeness. This lesson surveys the methodologies engineers built to attack them. And the first thing to understand is the trap: no single methodology defeats all the obstacles. Each one is strong on a particular axis and blind on another.

• Directed testing gives you perfect control of a scenario — but only the scenarios you imagined.
• Constrained-random gives you breadth you could never hand-write — but you don't know what it actually hit.
• Assertions give you deep observability — but they check contracts, not whole-system behaviour.
• Coverage gives you a measurement of completeness — but it measures your model, not correctness.
• Formal gives you exhaustive proof — but only for bounded properties within a tractable state space.

So the real engineering problem is not "which methodology is best?" It is:

Which methodology answers which obstacle — and how do you combine them into one flow so their blind spots cancel instead of compound?

Motivation — why any single methodology, used alone, fails

Each methodology, taken as the only tool, has a failure mode that is structural, not fixable by effort:

• Directed-only is blind to the unimagined. You write tests for the scenarios you thought of; the escaping bugs live in the ones you didn't. It also does not scale — you run out of engineer-hours before you run out of corners.
• Random-only is blind to what it did. Without coverage, a million random cycles is an unknown amount of verification — you cannot tell a thorough run from a lucky one, and you may pound the same easy states forever while a hard one goes untouched.
• Coverage-only is impossible — coverage is a measurement, not a stimulus or a check. It tells you where you haven't looked; it cannot drive or judge anything by itself.
• Assertions-only check local contracts, not end-to-end intent — a design can satisfy every assertion and still compute the wrong answer.
• Formal-only runs into the state-space wall: it proves bounded properties beautifully but cannot, in general, prove "the whole SoC is correct."

The motivation for a methodology (capital-M, the combination) is exactly this: the only way to cover one tool's blind spot is another tool.

Mental Model

Hold this picture:

Verification methodologies are a toolkit, and each tool is sharp on one edge. Directed is a scalpel (precise, narrow). Constrained-random is a fire hose (broad, undirected). Assertions are tripwires (fire the instant a contract breaks, deep inside). Coverage is the map (where have we been?). Formal is a proof (true for all inputs, within bounds). You do not pick one tool and finish a job; you reach for the tool whose edge matches the obstacle in front of you — and a finished verification environment has all of them working together.

The skill is matching tool to obstacle, and layering them so the fire hose's breadth is measured by the map, judged by the tripwires, and topped up by the scalpel where the map shows a hole the hose never reached.

Visual Explanation — the methodology map

Each methodology is strong on one axis and blind on another. Naming the pairing is the whole point: it tells you what each tool is for, and therefore what you still need beside it.

Read the map as a set of pairings: directed and CRV are both controllability tools (one narrow, one broad); ABV is the observability tool; CDV is the completeness tool; formal is the exhaustiveness tool for bounded properties. The moment you name what a tool is for, you see what it is not for — and that gap is the next tool.

RTL / Simulation Perspective — one feature, four lenses

Take a two-master arbiter with one rule: never grant both masters in the same cycle (mutual exclusion). Watch how each methodology attacks the same feature differently:

// RULE: gnt0 and gnt1 must never both be high in the same cycle.
 
// 1. DIRECTED — construct the specific race you thought of:
req0 = 1; req1 = 1; @(posedge clk);   // both request at once; check the grant
 
// 2. CONSTRAINED-RANDOM — let constraints generate request patterns you didn't enumerate:
constraint c { req0 dist {0:=1, 1:=2}; req1 dist {0:=1, 1:=2}; }  // random overlaps emerge
 
// 3. ASSERTION-BASED — encode the contract so ANY violation reports itself, from any stimulus:
assert property (@(posedge clk) !(gnt0 && gnt1));   // fires the cycle the rule breaks
 
// 4. FORMAL — prove the assertion holds for EVERY reachable input sequence (no stimulus needed):
//    the tool searches the whole bounded state space for a counterexample.

Notice the division of labour. Directed and CRV make the situation happen (controllability) — directed for the one race you pictured, CRV for the thousands you didn't. The assertion catches the violation (observability) regardless of which stimulus exposed it. Formal proves there is no violation at all, within bounds, without any stimulus. The same one-line rule is served by four tools, each doing the part the others cannot.

Verification Perspective — the modern flow layers them

A real environment does not choose; it stacks the methodologies into a pipeline where each covers the previous one's blind spot.

The layering is the whole methodology: breadth from constrained-random, judgement from assertions and a spec-derived scoreboard, measurement from functional coverage, and finishing from directed tests and formal where the random flow leaves a hole or where a bounded property deserves a proof. Remove any layer and a blind spot reopens.

Runtime / Execution Flow — the methodology as a closure loop

Stacked tools become a workflow: run the broad flow, measure it, and spend targeted effort only where measurement shows risk remains — then sign off on closure, not on the calendar.

This is why the methodologies are complementary in time, not just in principle: the broad random flow does the bulk of the work cheaply, coverage tells you where it fell short, and you spend expensive directed/formal effort only on the holes — the most cost-effective route to risk closure (the economics of the previous lesson, made operational).

Waveform Perspective — why breadth finds what control misses

Here is the concrete reason constrained-random earns its place beside directed testing. On a valid/ready handshake, a directed test usually writes the polite case (assert valid, get ready, transfer). Random stimulus naturally produces stall-then-burst patterns — exactly the back-pressure corners a human rarely writes by hand.

The waveform is the argument for the layering: random stimulus created the corner (controllability), an assertion would judge the handshake at that exact cycle (observability), and a coverage bin records that the back-pressure case was finally exercised (completeness). No single methodology produced all three lines of value — the combination did.

DebugLab — the all-directed shop that taped out a deadlock

directed suite:  142 tests, 142 PASS        ← 100% of a hand-picked set
functional coverage:  (none collected)      ← no measure of what was exercised
cross {arb_state=S, req_overlap=1}:  unknown ← never modelled, never hit, never reported

Common Mistakes

• "Constrained-random replaces directed testing." It doesn't — they are complementary controllability tools. Random gives breadth; directed pins the specific corners random reaches rarely or never. A mature flow uses both, with coverage deciding when directed top-up is needed.
• "100% code coverage means we're done." Code coverage proves every line ran, not that every behaviour was exercised or correct. Functional coverage (did the scenarios happen?) is the relevant measure, and even that bounds known risk, not correctness.
• "Assertions are optional / a nice-to-have." Assertions are the observability layer; without them, internal contract violations stay silent until they leak to an output cycles later (or never). They are how a methodology sees.
• "Formal is academic / not for real chips." Formal is standard for bounded, safety-critical properties (mutual exclusion, deadlock-freedom, register access, connectivity). It is exhaustive where simulation can only sample — used precisely, not instead of simulation.

Senior Design Review Notes

Interview Insights

Exercises

1. Match tool to obstacle. For each, name the single methodology you'd reach for first and why: (a) "we can never get the design into the error-recovery state in our tests"; (b) "this internal handshake violates its protocol but our output checker doesn't notice"; (c) "we must guarantee two grants can never assert together, ever"; (d) "we don't know whether our random tests have exercised all the burst lengths."
2. Justify the layering. Explain, in three sentences, why a flow with constrained-random + assertions + coverage is stronger than the sum of those three run separately — i.e., what each provides that makes the others more valuable.
3. Spot the blind methodology. A team reports "100% directed tests passing, taping out." State the one question that exposes their risk, and the two methodologies you would add first.
4. Pick formal vs simulation. For a register block with 200 fields and access-permission rules, argue whether the access-permission correctness is better attacked by simulation or by formal — and why the rest of the block might be the opposite.

Summary

• No single methodology defeats every obstacle: directed and constrained-random attack controllability (narrow vs broad), assertions attack observability, coverage attacks completeness, and formal attacks bounded exhaustiveness. Each is strong on one axis and blind on another.
• The modern flow layers them so the blind spots cancel: random for breadth, assertions + scoreboard for checking, coverage for measurement, directed + formal to close the stubborn corners — run as a closure loop until risk is closed.
• Coverage is the linchpin — the only methodology that measures the others, turning a toolkit into an accountable, closed-loop methodology and giving sign-off a definition.
• The durable rule of thumb: directed-only is blind to the unimagined; random-only is blind to what it did — layer them, and measure with coverage.
• UVM industrialises this layered, dynamic-simulation flow — reusable stimulus, checking, observation, and coverage components — so the combination is built once and reused. You now have the map of the approaches UVM packages.

Next — Directed Testing: with the landscape surveyed, we go deep on the oldest and most controllable methodology — when hand-written directed tests are exactly the right tool, how to write them well, and precisely where they stop scaling.