Presentation
AI‑Assisted Formal Verification: Improving Practical Adoption and Scalability
DescriptionAs chip complexity continues to grow, shift-left verification has become critical for improving verification efficiency and design quality. Formal Verification is a key enabler of shift-left adoption, as it provides exhaustive analysis and exposes corner case bugs early in the design cycle. Despite these advantages, many design verification (DV) teams struggle to adopt formal methods due to expertise gaps, scalability limitations, and the perceived difficulty of manual property authoring.
This presentation introduces a practical, AI-assisted roadmap for scaling formal verification across IP, subsystem, and SoC level designs. The approach combines early "quick win" formal applications (linting, UNR, connectivity) with scalable intermediate techniques (CSR, CDC/RDC, safety and security), and extends to advanced Formal Property Verification (FPV). Recent advancements in AI-assisted assertion generation, leveraging natural-language-to-property workflows, context-aware reasoning, and automated constraint derivation significantly reduce the manual effort required for FPV setup.
The methodology has been field tested across real design teams, demonstrating improved scalability, faster proof convergence, reduced assertion authoring effort, and higher overall adoption. Key complexity management techniques, including modularization, abstraction, and constraint strategies, are also discussed as essential enablers for deploying formal verification at scale in modern front-end verification flows.
This presentation introduces a practical, AI-assisted roadmap for scaling formal verification across IP, subsystem, and SoC level designs. The approach combines early "quick win" formal applications (linting, UNR, connectivity) with scalable intermediate techniques (CSR, CDC/RDC, safety and security), and extends to advanced Formal Property Verification (FPV). Recent advancements in AI-assisted assertion generation, leveraging natural-language-to-property workflows, context-aware reasoning, and automated constraint derivation significantly reduce the manual effort required for FPV setup.
The methodology has been field tested across real design teams, demonstrating improved scalability, faster proof convergence, reduced assertion authoring effort, and higher overall adoption. Key complexity management techniques, including modularization, abstraction, and constraint strategies, are also discussed as essential enablers for deploying formal verification at scale in modern front-end verification flows.
Event Type
Engineering Poster
TimeWednesday, July 293:00pm - 4:00pm PDT
LocationDAC Pavilion, Exhibit Floor