Formal Verification · All levels
Formal Coverage & Signoff: Tricky Q&A
Senior interview and review questions for Formal Coverage & Signoff.
Section Q&A bank
Use these drills after completing all topics in Formal Coverage & Signoff. Answer with requirement context, mechanism proof, artifact, owner, and signoff decision.
If all properties are green, why can formal coverage still be weak?
[INT][FORMAL][COVERAGE-AND-SIGNOFF]
Q: If all properties are green, why can formal coverage still be weak?
A:
Because proof status alone does not measure proof usefulness. Properties can pass vacuously, rely on over-strong assumptions, or cover only shallow control slices. Coverage is strong only when proven properties are reachable, assumption-realistic, COI-relevant, and mapped to architectural requirements.
FOLLOW-UP TRAP: Assuming a high proven-count automatically means high formal confidence.What does a failed critical cover objective usually indicate?
[INT][FORMAL][COVERAGE-AND-SIGNOFF]
Q: What does a failed critical cover objective usually indicate?
A:
It often signals a modeling or design intent mismatch: assumptions may block legal behavior, the scenario may be structurally unreachable due to RTL/spec issues, or the cover may be incorrectly encoded. Treating unreachable covers as first-class debug targets is key to trustworthy signoff.
FOLLOW-UP TRAP: Treating cover failures as optional because no safety assertion failed.What exactly is guaranteed by a bounded proof at depth 80?
[INT][FORMAL][COVERAGE-AND-SIGNOFF]
Q: What exactly is guaranteed by a bounded proof at depth 80?
A:
Only that no violating trace of length up to 80 cycles exists under the modeled assumptions. It does not guarantee correctness at cycle 81 or beyond unless supported by inductive or other unbounded reasoning.
FOLLOW-UP TRAP: Interpreting bounded depth as equivalent to complete proof closure.Why combine formal and simulation coverage if formal already explores state space exhaustively?
[INT][FORMAL][COVERAGE-AND-SIGNOFF]
Q: Why combine formal and simulation coverage if formal already explores state space exhaustively?
A:
Formal is exhaustive within scope and assumptions, but practical projects use abstractions and partitioned proofs. Simulation complements this by validating data-heavy and software-driven behaviors over long temporal contexts. Joint signoff reduces blind spots from either method alone.
FOLLOW-UP TRAP: Using formal results to skip simulation closure for all requirement classes.Q&A drill guide
REQUIREMENT -> PROPERTY -> EVIDENCE -> OWNER ACTION -> RESIDUAL RISKSketch while answering
FORMAL SIGNOFF PYRAMID
requirements -> properties and covers -> quality metrics -> waiver governance -> release decisionCommon traps
Separate status color from proof quality dimensions.
Treat unreachable critical covers as signoff blockers.
Document bounded-horizon rationale with architecture limits.
Key takeaways
Tie each proof claim to assumption boundaries and reachability evidence.
Prefer minimal reversible fixes and preserve legal behavior visibility.
Common pitfalls
Treating runtime reduction as proof-quality improvement without audits.
Declaring closure while critical covers remain unreachable.
Using broad waivers instead of first-divergence root-cause ownership.