25 / 37 · Concept
Verification plans, coverage and independent reference models
Distinguish passing tests from satisfying the specification, and link boundaries, crossed conditions and minimal counterexamples to a verification plan.
Lessons are free to read. Enroll to save your learning progress.
A verification plan turns a specification into checkable claims
Replace “works correctly” with concrete claims about post-reset state, normal outputs, holding during stalls, invalid-input handling and completion timing. Connecting each claim to at least one test and observation point makes omissions easier to find.
| Functional claim | Stimulus | Observation |
|---|---|---|
| Reset priority | Assert reset and enable together | Next state is the initial value |
| Preserved data order | Consecutive asymmetric patterns | Value and valid of every output |
| Exact boundary wrap | States around the maximum | M-1→0, no out-of-range value |
| Hold during a stall | Change inputs with accept=0 | Stored state remains unchanged |
| Overlapping patterns allowed | 10101 | Detection at accepted inputs 3 and 5 |
Why an independent reference model matters
Copying shift RTL into a reference model with the same slicesSlice An operation selecting a contiguous range of bits from a vector. The selected range determines the result width and bit order. Learn more can copy its indexing error too. Expressing the specification differently, with integer multiplication/modulo or a string-suffix comparison, helps cross-check it. Different notation alone does not prove independence, so verify small cases by hand.
Coverage is not a count of passing tests
Code-line execution coverage differs from checking functional cases. Crosses such as reset×enable, state×input and full×push×pop can expose errors. Add directed tests for rare, important combinations instead of relying only on random testing.
An N-input combinational circuit has input combinations, but sequential circuits also have time sequences of inputs. Analyze state reachability and whether invariantsInvariant A condition that must remain true in every permitted execution. For example, the occupancy of a depth-4 FIFO must always lie between 0 and 4. hold across all transitions. Do not describe a finite passing simulation record as a mathematical proof over unlimited time.
Generate answers independently from the specification rather than copying the implementation. On failure, record not just the actual result but the preceding inputs and state.
- Specification and stimulus: Choose boundaries and crossed conditions
- Independent reference model: Compute expected values and valid times
- Compare with the DUT: Compare at the same observation point
- Record the first mismatch: Keep the minimal counterexample and seed
Minimize and record failures
Save the prior state, inputs, expected value and actual value at the first mismatch. Remove unnecessary stimulus to retain a minimal counterexample, then fix the design. Re-run the existing boundary and resetReset A control that returns state to a specified initial value. Define whether it is synchronous or asynchronous and whether it has priority over other controls. Learn more regression checks alongside the modified test.
Try it yourself
RTL code coverage is 100% and 10,000 random tests pass, but reset=1 and enable=1 never occurred together. What should be added?
Read the explanation
Check that crossed condition in the specification and add a directed test from a nonzero initial state that exposes priority. Code coverage and test count do not replace checking a specific functional condition.