Formal Verification Foundations: Tricky Q&A

[INT][FORMAL][FPV-FOUNDATIONS]

Q: Why can a formal proof pass while silicon behavior is still wrong?

A:
Because the proof only guarantees behavior inside the modeled assumptions and initialization semantics. If constraints unintentionally exclude legal traffic, ignore reset corner cases, or impose unrealistic fairness, the solver proves a narrowed world instead of the real design environment. Soundness comes from both proof convergence and assumption validation.

FOLLOW-UP TRAP: Treating a green proof status as unconditional correctness without auditing assumptions and initialization model.

[INT][FORMAL][FPV-FOUNDATIONS]

Q: When should a requirement be written as safety versus liveness in FPV?

A:
Use safety when the intent forbids an illegal condition at any time, and use liveness when the intent requires eventual progress or response. Many protocol rules need both: safety to block illegal overlaps and liveness to guarantee completion. Misclassifying a progress rule as pure safety can miss starvation and deadlock behaviors.

FOLLOW-UP TRAP: Encoding all requirements as safety assertions and assuming deadlock freedom is automatically covered.

[INT][FORMAL][FPV-FOUNDATIONS]

Q: How does cone-of-influence reduction speed proofs without changing property meaning?

A:
COI removes state and logic that cannot affect the assertion outcome, reducing solver burden while preserving the same truth condition for that property. The speedup is real only if removed logic is genuinely irrelevant; reduction paired with accidental over-constraint produces misleading convergence. That is why COI should be paired with reachability covers and constraint sanity checks.

FOLLOW-UP TRAP: Assuming any proof speedup from COI is valid even when reachability drops unexpectedly.

[INT][FORMAL][FPV-FOUNDATIONS]

Q: What is the most common reason FPV projects stall even with a good assertion plan?

A:
Constraint quality and run strategy, not assertion count. Overly loose assumptions explode state space, while overly tight assumptions hide legal behavior; both delay closure. Teams that iterate constraints, bucket properties by complexity, and debug vacuity early reach stable convergence far faster than teams that only add more assertions.

FOLLOW-UP TRAP: Believing poor convergence is solved primarily by writing more properties instead of improving constraints and run partitioning.

REQUIREMENT -> PROPERTY -> EVIDENCE -> OWNER ACTION -> RESIDUAL RISK

FPV FOUNDATION LOOP

requirements -> property set -> assumptions and reset model -> prove/fail traces -> closure audit