The subsystem architect puts a block diagram on the screen: the two DMAs, an AXI interconnect, a register file shared with the CPU, a clock-domain bridge to a slow peripheral bus, and the CPU itself. For each block, tell me how you will verify it and what will sign it off. Answering "UVM for everything" is the fastest way to sound junior. What does a strategy that matches the method to the block look like?
Every verification method answers a different kind of question at a different cost. Simulation with a UVM bench samples behaviour and checks it against a model; it handles data paths and long flows and never proves completeness. Formal reasons about every input sequence within assumptions; it proves control rules and finds corner cases in small state spaces, and struggles with wide arithmetic and deep sequences. Emulation and FPGA prototyping trade visibility for speed, so they can run software and long scenarios. Gate-level and power-aware simulation check what RTL simulation cannot see: the netlist, unknowns and power domains. Structural CDC and reset-domain tools check clock and reset crossings by analysis, not stimulus.
A doctor chooses diagnostics the same way. A suspected fracture gets an X-ray, an infection gets a blood test, soft tissue gets an MRI. Ordering an MRI for everything is slow and expensive and still misses the infection. A verification strategy is the list of which test each block gets, and why.
Block type | Primary method | Add | Sign-off evidence |
|---|---|---|---|
Control FSM, arbiter | Formal: properties for transitions, fairness, no deadlock | Simulation for system scenarios | Full proofs or justified bounded depth; covers reached; FSM code coverage |
Data path (ALU, DSP, crypto) | Simulation against a reference model, often C through DPI | Formal equivalence for re-pipelined versions; formal for control around it | Plan coverage, model-compare pass, code coverage with reviewed exclusions |
CDC-heavy bridge or FIFO | Structural CDC and RDC analysis | Formal for handshake and FIFO protocols; simulation with random clock ratios | Clean CDC report with reviewed waivers; protocol proofs |
Register file, CSR block | Generated register model with built-in sequences, and formal register apps | Directed tests for side effects (W1C, triggers, busy rules) | Reset and access checks pass; side-effect rows checked |
Interconnect, fabric | Simulation with protocol VIP and a scoreboard per path | Formal connectivity and deadlock checks; performance runs | Every master-slave path covered, ordering rules checked, protocol VIP clean |
CPU-based subsystem | Software tests on the CPU in simulation, then emulation | UVM around the CPU for peripherals; FPGA for software teams | Boot and driver tests pass; integration plan rows closed |
Power-managed block | Power-aware simulation with the UPF | Formal or static checks of isolation and retention structure | Every power state and transition covered; isolation and retention checks pass |
Gate-level simulation sits across all of these: a reduced list of tests on the netlist, after equivalence checking and STA, looking for reset, X and timing-check problems the RTL hides. Simulation for Sign-off explains what it finds and why it still exists.
Plan area (testplan IDs) | Method | Why | Evidence in the course |
|---|---|---|---|
Register rules: busy writes ignored, W1C, interrupt equation, GO while busy, set wins over clear (R2, S2, S4, R3, S5) | Formal, with APB as assumptions | Small state, many interleavings that random stimulus rarely hits | R2, S2 and S4 proved in a scratch run, where the old illegal-bin claim fell in 12 cycles; R3 and S5 are the next two properties |
Reset values and access policies (R1) | Register model sequences | Generated from the register description; cheap |
|
Data path end to end, lengths, errors, backpressure (D1-D5, E1, E2, H1, H2) | UVM simulation with scoreboard and coverage | End-to-end promises over long transfers; driver and reset interplay | The block bench; closure tests |
DONE and TLAST timing (S1, D2) | Assertions, in simulation and formal | Cycle-level rules; the fault campaign showed no check existed | To add; faults 6 and 7 escaped |
APB and AXI-Stream protocol | Bound assertion VIP | Same file in block, chip and formal runs | |
Reset mid-job, X after reset (X1) | Simulation, plus a four-state X check and GLS smoke | Verilator is two-state; X needs a four-state simulator or the netlist |
|
Clock domains | Not needed | The DMA is single-clock; if APB moved to its own clock, structural CDC first | |
Power | Not needed at block level | No power domain inside the block; at chip level, power-aware simulation if its domain switches | |
Driver and OS flow | Emulation at chip level | Billions of cycles; too slow for simulation |
Notice what the table does for the estimate: proving the register rules formally replaces several directed tests and covers S5, a race no random test was likely to hit. Strategy is also a schedule decision.
A formal result and a simulation result promise different things, and a strategy states which promise each row needs. The formal scratch run on the DMA's register rules, from the formal lesson (an excerpt):
## 0:00:00 Checking assertions in step 24..
## 0:00:00 Status: PASSED (bounded check: no failure in 25 cycles)
## 0:00:00 Temporal induction successful.
## 0:00:00 Status: PASSED (induction step: with the bounded check, a full proof)
## 0:00:00 Reached cover statement in step 8 at dma_formal.dut: c_errAnd the simulation side's measure of its own checks, the fault campaign:
faults detected by at least one test: 5 of 8The formal result is a proof for every legal APB sequence and every stream input, including LEN = 65,535, with a cover showing the assumptions allow a real error path. No number of seeds gives that.
The simulation result is a measurement of how good the bench's checks are on the behaviours it reaches. Its three misses are rows to fix, and two of them (DONE and TLAST timing) are cycle rules that formal and assertions handle well.
A team verified a clock-domain bridge with a thorough UVM bench: random clock ratios, backpressure, long regressions, coverage closed. It shipped, and the first silicon showed rare corrupted words on the slow side. A multi-bit status bus crossed domains without a synchronizer, so its bits could be captured from two different cycles. RTL simulation has no metastability and samples every bit on the same edge, so the bug was invisible to every test the bench could ever run. A structural CDC tool would have flagged the unsynchronised multi-bit crossing in minutes.
The strategy failed, not the bench. Clock crossings are a structural question, so the strategy needed a structural method first, with simulation as the complement. The same pattern repeats elsewhere: power-domain isolation is invisible to plain RTL simulation, netlist X is invisible to two-state simulation, and connectivity under every configuration is too many configurations to simulate. The interview skill is noticing which question a block is really asking.
Wide arithmetic is where formal property checking struggles: the solver's problem explodes. Verify the multiplier by simulation against a reference model (often a C model through DPI) with coverage of special values and rounding modes, and use formal where it is strong: equivalence against a previous version when the design is re-pipelined, and properties on the control logic around the data path.
Clock domains change from "not needed" to required: a structural CDC and RDC analysis of every APB-to-core crossing (GO, KEY, LEN, STATUS reads, the interrupt) with reviewed waivers, plus formal on the handshake used for the crossing. The UVM bench adds random clock ratios and checks that register writes land correctly. Register rules that were proved in one clock domain must be re-proved with the crossing in place.
Next: with the plan, the estimate, the architecture and the strategy in hand, the next topic, UVM with SVA and Formal, shows how assertions live inside the bench that this strategy relies on.