Verification: Prove the RTL Is Correct

Start with a verification plan

A verification plan maps each requirement to stimulus, checking, and coverage. “Output remains stable while stalled” needs randomized out_ready, end-to-end data comparison, and a protocol assertion. A waveform that merely looks plausible is neither scalable nor regression-safe.

A practical testbench has a driver, monitor, reference model, and scoreboard. The driver obeys the interface; the monitor reconstructs completed transactions from pins; the model computes expected sums; the scoreboard compares expected and actual output. Do not let the driver inspect internal DUT state.

Combine directed and constrained-random tests

Begin with batch length one, maximum length, all-zero and all-one data, and immediate output acceptance. Then randomize data, batch length, input bubbles, and backpressure. Log every random seed so a failure is reproducible.

property p_output_stable_when_stalled;
  @(posedge clk) disable iff (!rst_n)
    out_valid && !out_ready |=>
      out_valid && $stable(out_sum);
endproperty
assert property (p_output_stable_when_stalled);

Assertions are ideal for invariants such as legal states, bounded counters, stable stalled outputs, and one completion per accepted start. They complement rather than replace the scoreboard.

Use coverage as a question

Code coverage shows which RTL structures executed; functional coverage shows which requirement space was explored. Cover batch-length ranges, continuous and gapped input, stall duration, reset in every FSM state, overflow, and interrupt-enable combinations. Cross coverage exposes cases where individual features were tested but their important combinations were not.

High line coverage does not prove correctness. Unit-test the reference model and intentionally inject a small RTL defect to confirm the regression fails. This mutation check catches a testbench that is permanently green because its checker never observes the defect.

Chapter deliverables

• A requirements traceability table linking tests, assertions, and coverpoints.
• A one-command reproducible regression with seed and transaction history on failure.
• At least five protocol assertions and an independent scoreboard.
• A coverage report with explanations for exclusions and remaining holes.