Large language models are approaching the ability to perform one of the most frustrating tasks in chip design verification: converting natural-language specifications into a set of formal properties that can be used to assess the correctness of an RTL implementation. Interviews conducted by Brian Bailey in Semiconductor Engineering indicate that current tools can produce a useful initial draft, but they remain far from creating a complete set that can be adopted without extensive engineering review.
The importance of this development lies in the fact that writing properties has been a bottleneck in formal verification for years. SystemVerilog properties, known as assertions when included in a verification environment, are used to describe logical and temporal relationships between signals, such as reset behavior, handshakes, one-hot conditions, and basic safety checks. When these properties are complete and accurate, they can be used to compare the behavior of an RTL implementation with the specification, independently of how the design was built.
What Can the Tools Do Today?
A tool based on a large language model can read a specification document, a protocol standard, or even comments within RTL, and then propose a draft of SVA properties. Ashish Darbari, CEO of Axiomise, says this use is more practical when the specifications are based on stable standards that do not change frequently. In that case, the tool reduces the repetitive part of writing the initial code rather than taking over the entire verification process.
Some approaches attempt to improve model accuracy by creating a knowledge graph, meaning a graph of knowledge that stores entities and the relationships between them. The nodes may include a signal, module, requirement, or port, while the edges describe relationships such as “drives,” “resets,” and “responds to.” Instead of retrieving text passages that merely appear related to the request, the system can refer to specific facts and links, reducing the likelihood of inventing a signal name or misunderstanding a relationship between design components. In this context, the source points to a paper titled RAG-SVA in the Landscape of LLM-Based Assertion Generation by Cohen and Chibani.
The Problem Begins Before AI
The tool cannot extract what was never written or decided in the first place. Ravindra Aneja, director of applications engineering at Synopsys, says that an ideal specification has not been available over the past three decades; development often begins before the documentation is complete, and some projects may not have a complete specification at all, particularly in derivative designs or when requirements change during development.
This problem is not limited to wording; it also concerns change management. A marketing team may add a new feature or modify an existing requirement, and the design and verification teams must determine the impact of that change. Abhi Kolpekwa, senior vice president and general manager at Siemens EDA, believes that converting a specification into properties requires “contextual intelligence” that tracks the history and context of changes, rather than an agent that generates new text every time.
The Risk of False Confidence
The greatest limitation of the current approach is that a property may be syntactically correct, compile successfully, and be proven by verification tools, yet fail to test the intended behavior. Darbari warns that a weak or vacuous property may succeed easily because it permits many behaviors, uses the wrong signal, or contains a missing or overly restrictive antecedent. Therefore, a “green proof” does not mean that the design is free of errors; the proof is no stronger than the property that was proven.
The source adds that models tend to perform better in structural and syntactic coverage than in understanding architectural intent and the reason a rule exists. As a result, an inaccurate reading of the specification by the model may become a formal-looking and rigorous piece of text while concealing a requirements gap. If that gap carries over into activities such as FMEDA, safety files, or certification evidence associated with ISO 26262 and ISO 21434, its impact may extend far beyond the original verification project.
The separation of design and verification is also a concern. Kaye Mao, product design lead at Normal Computing, points to the need to restrict the project materials that agents can access, because allowing an agent to use the design itself to generate test cases could undermine the independence of the verification process.
What Changes in Practice?
According to Darbari, AI can reduce the time required to prepare initial drafts from days to minutes, but it may multiply the subsequent workload. Each generated property requires checking against the specification, coverage analysis, vacuity testing, and review of its relationship to design signals, while failures may require signal-waveform analysis. If the number of properties increases tenfold while the level of scrutiny required for each remains unchanged, the review burden may outweigh the benefit produced by faster generation.
From certi.news’s perspective, the real change is not replacing the verification engineer, but shifting the center of gravity from writing properties to evaluating them and tracing their sources. Darbari recommends treating generated properties as drafts rather than approved outputs and establishing a review gate before incorporating them into the regression suite. The source of each property should also be recorded—the specification paragraph, requirement, or RTL element that produced it—so that the engineer can verify its correspondence.
This approach may lower the barrier to entry for verification engineers who want to use formal verification, says Yaron Ilani, a verification solutions engineer at Normal Computing. However, it does not resolve the question of return on investment. Kaye Mao believes that the time required to verify the agent’s outputs must be counted as part of the cost, while Arvind Srinivasan, head of solutions engineering at Normal Computing, points out that scaling is not solely about computing; it also depends on data completeness and the cost of human review.
The conclusion is that large language models have become capable of accelerating the automated and repetitive part of formulating properties, but they have not yet solved the problems of specification completeness and understanding design intent. The value of these tools will remain tied to the presence of an engineer who understands the design, along with independent mechanisms for measuring coverage and detecting vacuous or unsuitable properties—not to the number of properties the model can produce.