AI-Powered Static and Formal Verification

Siemens Advances Unified Static and Formal Verification with AI

Static and formal verification have long promised stimulus-free analysis—techniques that can mathematically prove correctness across all inputs without needing to run simulations. However, these methods have faced significant adoption barriers: static analysis is often noisy, and formal verification traditionally requires specialized expertise. While both techniques are powerful in their own right, Siemens is now proposing a unification of these methods with the help of AI to overcome their limitations and significantly broaden their practical impact.

At the heart of this initiative is Siemens’ newly introduced solution: Questa One SFV (Stimulus-Free Verification). This platform combines static and formal methods with artificial intelligence into a unified verification environment aimed at making verification smarter, more efficient, and more scalable.

Breaking the Barriers of Stimulus-Free Verification

Dynamic verification techniques, while widely used, are limited to the specific test cases they cover. In contrast, static and formal methods can offer general proofs—but within a limited scope. Siemens’ objective is to loosen these constraints by merging the strengths of static and formal techniques under a single framework enhanced with AI.

Questa One SFV simplifies license management by drawing on a single pool of licenses, regardless of whether users are performing static checks, formal verification, or AI-powered operations. This not only streamlines access but also improves license utilization, especially when verification tasks are running in parallel.

AI at the Core of Enhanced Verification

One of the standout capabilities of Questa One SFV is its use of AI for natural language processing. It can interpret user-defined checks written in plain language, generate the corresponding formal property assertions, and verify them. This opens up formal verification to users who may not have deep expertise in formal languages or methods.

Additionally, Siemens leverages AI to tackle a well-known issue in static analysis: noise. Linting tools often produce overwhelming amounts of warnings, many of which may not be relevant. By applying formal filtering through Questa One SFV, irrelevant results can be suppressed, allowing teams to focus only on the critical issues.

Supporting Custom Protocols with Generative Verification

While Siemens already offers a formal VIP library covering standard protocols like AMBA, it acknowledges the real-world need for custom compliance verification. Many companies adapt standard protocols, such as creating a customized version of AHB. Siemens proposes that Questa One SFV can support such use cases using generative AI methods—starting from a custom specification and building a formal property suite tailored to it. The platform may also automate the partitioning of large formal proofs, improving scalability and practicality for complex designs.

Expanding the Role of AI in Verification

Siemens also hints at broader AI applications in the verification flow. For example, unsupervised learning techniques are already being deployed to group similar CDC and RDC (Clock and Reset Domain Crossing) violations, helping teams quickly identify likely root causes among large volumes of error reports.

Another novel use case discussed during DAC was AI-based detection of naming convention violations—a detail often overlooked by designers but increasingly critical for maintaining consistent design structures. Naming consistency not only aids human readability but also improves the performance of equivalence checking tools and AI training models used for design and test automation.

Conclusion: Toward Scalable and Smarter Verification

Siemens’ unified approach, combining static, formal, and AI capabilities under the Questa One SFV banner, signals a significant step forward in the evolution of digital verification. By lowering the expertise barrier and applying AI to streamline analysis, Siemens is making stimulus-free verification more accessible, scalable, and effective. As chip complexity continues to grow, this type of integrated, intelligent verification platform will be essential to keeping pace with the demands of modern system design.

Source - Semiwiki