VERIFICATION

Verification Plan: Executable Contracts, Coverage, and Formal

Connect requirements to simulation checks, coverage, and bounded or unbounded proofs. A passing proof is meaningful only under reviewed environment assumptions and reachable scenarios.

Inputs

Requirements, interface contracts, and bug history
Legal environment behavior and reset assumptions
Risk-ranked state-space and coverage goals

Method

Translate each requirement into an observable property, scoreboard rule, or coverpoint and assign an owner plus closure evidence.
Place interface assertions near the interface; distinguish DUT guarantees (assert) from legal stimulus constraints (assume).
Use constrained-random tests for interactions and monitors for protocol facts; cross coverage only for decisions that affect risk.
Prove small control invariants early, run cover properties to demonstrate intended progress, and inspect counterexamples as waveforms.
Review assumptions for overconstraint and vacuity; add covers that show the antecedent and key corner states are reachable.

Deliverables

Requirements-to-tests/properties/coverage matrix
Reusable interface assertions and monitors
Formal proof/cover report with assumption review

Pitfalls

Assuming away illegal behavior that the DUT must reject or recover from.
Using coverage percentage as evidence that correctness properties were checked.

Sources

UVM 1.1 User’s Guide ↗
Accellera · §3.12.2 Implementing Checks and Coverage in Interfaces

Formal extensions to Verilog ↗
YosysHQ · §6.1 SystemVerilog Immediate Assertions

Getting started ↗
YosysHQ · SymbiYosys