A formal proof is conditional: the property holds for every behavior allowed by the model. Assumptions define which environment behaviors are legal. If they are too weak, the engine spends time on impossible traffic. If they are too strong, they can remove the failing trace and make an incorrect design appear correct.
Treat assumptions as specifications
Each assumption should have an owner, a source requirement, and a reason for existing. Protocol assumptions belong at the boundary that owns the protocol. Internal design behavior should rarely be assumed; doing so can convert the implementation under test into part of the trusted environment.
Review assumptions independently from assertions. Ask whether a real integrator can violate the condition, whether reset and startup are covered, and whether two individually reasonable assumptions conflict. Reuse protocol assumptions carefully because optional features and parameter values can change the legal environment.
Use covers as model sanity checks
Cover properties demonstrate reachability; they do not prove correctness. They are useful for showing that reset completes, requests occur, backpressure is possible, each arbitration client can win, and relevant error paths remain reachable. A collection of covers should exercise assumptions and the antecedents of important assertions.
- Cover the shortest legal transaction.
- Cover each important state and transition.
- Cover contention, backpressure, cancellation, and recovery.
- Cover activity after reset and after reconfiguration.
- Cover simultaneous conditions that are easy to constrain away accidentally.
Understand vacuity
An implication can pass because its antecedent never occurs. That may be correct for unreachable behavior, or it may mean the environment prevents the obligation from triggering. Track antecedent coverage, use witness traces, and review properties that prove unexpectedly quickly.
Reset is a common source of vacuity. A broad disable condition can keep properties inactive throughout explored behavior. Likewise, an unconstrained reset that may remain asserted forever can make post-reset obligations irrelevant. Model reset release and required stabilization explicitly.
Challenge the proof model
Temporarily weaken assumptions, add covers for forbidden-looking behavior, and inspect counterexamples. Where tools support proof-core or cone analysis, use it to see which assumptions and design elements contribute to a result. A property that depends on an unexpected assumption deserves review.
Proof status answers the property; model review establishes whether it was the right question.
Sign-off should include the property, result class, assumptions, cover evidence, abstraction notes, and tool configuration. This turns a green icon into a reviewable engineering artifact.
Primary references
Need help applying these methods to a verification programme? Start a technical conversation.