Presentation
Invariant-Driven Contract-Based Formal Verification for Scalable Compositional Proofs
DescriptionFormal verification based on contract-based and assume–guarantee reasoning is a powerful technique for scalable system validation, yet it often suffers from state-space explosion when implicit design invariants are not explicitly captured. In practice, modern SMT-based model checkers spend significant effort exploring unreachable or irrelevant regions of the state space, leading to non-convergence even for correct designs. This work proposes an Invariant-Augmented Contract-Based Formal Verification methodology that systematically integrates State Space Tunneling (SST) as a counterexample-driven refinement mechanism. When a target property fails to converge, tunneling is used to generate non-reset counterexamples that expose unreachable but solver-visible behaviors. These behaviors are analyzed to extract missing inductive invariants, which are encoded as helper assertions and fed back into component contracts or assertion sets. Once proven, the invariants are safely assumed in subsequent proofs, effectively pruning unreachable state regions without over-constraining the design. The approach introduces an iterative refinement loop that progressively strengthens contracts, improves compositional reasoning, and accelerates convergence of complex proofs. By combining industrial SST workflows with contract-based verification, the proposed method bridges the gap between architectural intent and low-level formal analysis. This work demonstrates how invariant augmentation transforms SST from a debugging aid into a systematic scalability mechanism for large, complex hardware designs.
Event Type
Engineering Poster
TimeMonday, July 275:00pm - 6:00pm PDT
LocationDAC Pavilion, Exhibit Floor