About the Speaker

Surinder Sood holds a PhD in Design Verification and Validation of Hybrid Systems from the University of Auckland, New Zealand, with over 20 years of experience in hardware and SoC verification. His expertise spans diverse verification techniques, with research interests in formal verification of digital and hybrid systems. He has also worked on security vulnerability analysis and performance estimation of SoCs. He has contributed to leading organizations including Intel, AMD, Samsung Electronics, STMicroelectronics, and SanDisk. He is currently a Principal Engineer at Arm, Visiting Researcher at the University of Manchester, and a Senior Member of the IEEE Circuits and Systems Society.

A Contract-Based Framework for Scalable Compositional Verification Using Invariants

Overview

Formal verification of modern hardware designs is challenged by deep pipelines, concurrency, and complex protocol interactions, limiting scalability of monolithic proofs. This work proposes a contract-based compositional framework using invariants. System behavior is decomposed into module-level assumption–guarantee contracts, where inductive invariants capture protocol, arbitration, and resource constraints such as credit handling and ordering. These invariants enable sound composition while ensuring local proofs imply global correctness. The framework emphasizes invariant reuse, hierarchical reasoning, and abstraction of dependencies, enabling efficient verification of large designs. Case studies show improved convergence, reduced complexity, and better reuse of verification collateral.

Key Points

• Invariants
• composition
• contract