Bridging the Gap: A Practical Roadmap to Formal Verification for DV Engineers

Formal Verification (FV) has emerged as a powerful complement to dynamic simulation-based verification, offering exhaustive and mathematically rigorous analysis of digital designs. Despite its proven benefits, many Design Verification (DV) engineers face challenges in adopting FV due to a lack of clarity on where to begin and how to progress effectively. This paper presents a structured methodology — The Formal Pathway — designed to guide DV engineers through a practical and progressive adoption of Formal Verification.

The methodology is divided into three key stages: 1. Focuses on low-effort, high-impact applications such as Unreachability (UNR), Connectivity, Assertion IPs (AIP) apps, Linting, and Low Power checks. 2. Introduces more advanced use cases including Control and Status Register (CSR) verification, Clock and Reset Domain Crossing (CDC/RDC) analysis, and Security and Safety properties. 3. Addresses complex design scenarios, emphasizing Formal Property Verification (FPV), Sequential Equivalence Checking, and Datapath verification. Recent advancements in EDA tools are further easing the adoption of FPV. AI-powered features such as automatic generation of assertions based on design specifications are helping DV engineers overcome the initial barriers to formal property authoring. These innovations are making FPV more accessible and reducing the learning curve, enabling teams to integrate formal techniques earlier and more effectively. In parallel, the paper discusses strategies to manage and mitigate complexity, enabling scalable formal deployment across diverse design environments. By offering a clear roadmap and actionable insights, this paper aims to empower DV engineers to confidently integrate Formal Verification (using VC Formal) into their workflows, ultimately enhancing design quality and verification efficiency.

Gilberto Migliorin is a Principal SOC/Subsystem Verification Engineer at Synopsys Inc., currently working within the Systems Solutions Group. With over two decades of experience in digital design verification, Gilberto has contributed to successful projects in the automotive domain and across a range of general-purpose microcontroller platforms. Throughout his career, he has taken initiative in both leading verification programs and independently owning critical technical areas, spanning SOC-level and subsystem-level verification, embedded software, and post-silicon validation. His expertise includes ARM and Tensilica architectures, and he has collaborated with global teams across multiple engineering disciplines. Gilberto holds a Master’s degree in Computer Science from Universidade Federal do Amazonas, with a focus on Digital Video Processing, and a Bachelor’s degree in Electrical Engineering from Universidade Federal do Rio Grande do Sul. He is recognized for his technical depth, cross-functional collaboration, and contributions to verification methodology improvements.