Formal Verification First: How AI Supports But Cannot Replace It

At a recent VLSI-D panel, industry leaders explored one of the most pressing topics in silicon design today — the intersection of AI-powered EDA, which is revolutionizing chip design for tomorrow.

Ashish Darbari, CEO of Axiomise, questioned the panelists on the role of AI in chip design, optimizing PPA, validation and verification. While the panel explored the role of AI in design implementation, from bring-up all the way to floor planning, panelists showed the greatest enthusiasm answering questions around validation and verification and how AI can impact both.

Only 14% of ASICs are designed correctly the first time, which is where formal verification and AI can help (2024 Wilson Research Group IC/ASIC Functional Verification Trends, 2024). AI continues to positively impact simulation and emulation, and both intersect with formal.

AI’s ability to process massive data sets and explore vast design spaces has captured widespread attention, but AI cannot replace formal verification. The reason is that formal provides mathematical certainty. It proves that a design satisfies its specification across all possible behaviors within defined constraints. This determinism is what makes formal verification indispensable, and it’s what generative AI cannot offer — at least until models stop hallucinating and are accompanied by explainable AI and other formal assisted reasoning mechanisms.

It is worth noting that the birth of AI happened in 1956 (Dartmouth, 2025).

The impact of AI on large-scale system design verification

The scale of modern silicon designs only reinforces this point. Hyperscalers are investing hundreds of billions of dollars in data center CapEx, racing to support AI workloads. Traditional scale-up systems are giving way to rack-scale superclusters, scaling from a few XPUs to more than 1,000 per rack. Optical interconnects are replacing copper, and connectivity is now a first-class design challenge. These architectures make design spaces larger and more complex than ever.

At this scale, gate-level and physical optimization is humanly impossible without assistance. AI can help, but only when specifications, data, and context are well defined. Without that structure, engineers risk “garbage in, very expensive garbage out.” Faster output is meaningless if correctness cannot be guaranteed.

The panelists agreed that where AI truly adds value is in supporting verification, not replacing it. It excels at pattern recognition, prioritization, and exploration – identifying coverage gaps, suggesting areas for deeper analysis, and assisting in generating stimuli or testbench components. AI can guide engineers toward the parts of the design where effort is most likely to pay off, but it cannot prove correctness. That proof remains the domain of formal verification, which is inherently deterministic. A property either holds, or it does not. A counter-example either exists, or it does not.

There is no probabilistic middle ground. This distinction is critical. AI-generated outputs must always be validated by deterministic engines. Without that validation, AI merely produces faster answers, not necessarily correct ones. In verification, speed without correctness is not progress.

Limits of verification lie in specification

Specification quality is another key challenge. Formal verification depends on clear intent, yet specifications are often incomplete, ambiguous, or difficult to operationalize. AI can help extract structure and connect information, but it cannot define intent on its own. Only engineers can do that.

Formal verification is what ensures that intent is truly captured in silicon. However, this is an area where AI agents are showing great promise. By harvesting the NLP and LLM technologies, the agents can harvest often implicit knowledge and help in assisting engineers with missing specifications.

Expert in the loop

As AI tools become more accessible, over-reliance can be a real risk. Engineers may be tempted to trust outputs without fully understanding them. Foundational knowledge —understanding properties, constraints, assumptions, and coverage — is more important than ever. AI literacy is valuable, but verification expertise is non-negotiable. A human-in-the-loop is necessary.

Other topics discussed by panelists included how data can be kept secure and how data contamination between different customers can be avoided.

The future of verification is not a choice between AI and formal methods. It is about integrating AI into formal verification in a way that respects its deterministic nature. AI can help teams reach formal sign-off faster, but it cannot replace the guarantees that formal verification provides. Formal verification remains the final authority. AI is an assistant — powerful, helpful, and increasingly important, but always accountable to proof.

These principles, reinforced in the insights shared by industry experts on the panel, guide how we build tools, design workflows, and work with customers at Axiomise. In silicon verification, certainty is not optional, and nothing replaces proof. Formal verification is the foundation of Axiomise, not the destination. Our automated tooling, including formalISA, accelerates coverage analysis, reduces manual effort, and highlights gaps, all while remaining grounded in provable, deterministic methods. Our approach ensures that AI assists verification without undermining certainty.

References

Dartmouth. (2025). Artificial Intelligence (AI) Coined at Dartmouth | Dartmouth. Home.dartmouth.edu. https://home.dartmouth.edu/about/artificial-intelligence-ai-coined-dartmouth

2024 Wilson Research Group IC/ASIC functional verification trends. (2024). Siemens Digital Industries Software. https://resources.sw.siemens.com/en-US/white-paper-2024-wilson-research-group-ic-asic-functional-verification-trend-report/