Coverage metrics for formal
Simulation has a familiar answer to "are we done?": code and functional coverage. Formal needs different metrics, because a proof covers all input sequences — the question is whether the properties cover the design.
| Metric | Measures | Weakness |
|---|---|---|
| Cover reachability | The environment allows the planned behaviours | Only as good as the list of covers |
| Vacuity | Assertions are actually exercised | Says nothing about missing assertions |
| COI coverage | Logic that could affect some assertion | Optimistic: being in a cone does not mean being checked |
| Proof-core coverage | Logic the engines actually needed to prove assertions | Tool-specific; needs full proofs |
| Mutation coverage | Injected bugs that some assertion detects | Run time; choice of mutations |
| Bounded-proof coverage | Which behaviours lie within the proven depth | Needs covers to interpret |
Combining with simulation
Most projects merge formal and simulation results into a single verification dashboard: items fully proven by formal are marked as covered, items proven unreachable (UCE) are excluded, and the rest remain simulation's responsibility. Agree with the project how proven assertions count toward functional coverage — typically, a proven assertion plus its reachable antecedent cover counts as the corresponding functional item being covered.