AI 自动生成属性（Properties）：从规范到验证的方法学插入分析

Key Takeaways:

• While AI can write properties from a specification, the specifications that exist today are rarely good enough to be able to generate anything useful from them.
• Automatic generation of properties does not reduce the need for people who are fluent in the language, or the application of formal tools.
• Introduction into a methodology will probably be different for each company today, with no well-proven methodologies to learn from.

A top-down semiconductor development flow has long been a goal for chip design, and shift left is certainly making that increasingly possible. The problem is that the starting point — the specification — is often incomplete or nonexistent, because the chip industry has been notoriously bad at writing specifications.

There are several ways to insert AI into existing flows. But just because something can be done doesn’t mean it should be. This is one of the big challenges facing AI adoption. Many existing tasks could be done more efficiently using an agentic flow, but it’s not clear whether that is the right thing to do.

This limitation becomes especially apparent when AI starts to help with something that has been woefully inadequate in the past — the creation of good, complete specifications. The big question is whether AI can enable designs, or verification environments, to be automatically derived from a specification. Perhaps a more correct goal is whether AI can help create better specifications. With better specifications, downstream design becomes a lot easier.

“AI can generate a SystemVerilog assertion in seconds,” says Ben Cohen, verification technologist and book author. “Whether that assertion means anything depends entirely on what it was generated from, and in practice that source is rarely a single, clean, natural-language specification. It is just as often an ambiguous paragraph that needs clarifying before it can be trusted.”

Solving this problem should be considered a high priority. “The increasing complexity of modern SoC designs is making AI-assisted artefact generation and verification closure a practical requirement rather than a research option,” says Simon Davidmann, AI and EDA researcher at the University of Southampton. “The verification problem is, in practice, already at the scale where it cannot be addressed without AI assistance. The 5-to-1 ratio of verification engineers to designers in processor development is not a workforce planning anomaly, but a signal that the complexity has outgrown the methods.”

Going from specification to anything is not a reality today. “If we are actually going to make this reality, we need more discipline in terms of writing the spec,” says Ravindra Aneja, director of applications engineering at Synopsys. “If we really want to make it a reality, we have to work on it. As an industry, are we there? No, we are not there. I don’t think we are at a place where, either starting a new design or doing a derivative design, you can say the spec is good enough.”

Are we even thinking about it in the right way? “A prose specification document is not something a formal tool can reason over directly, because formal engines operate on precise, unambiguous, machine-checkable statements, not natural language,” says Ashish Darbari, CEO of Axiomise. “What AI can help with is narrowing that gap, translating prose into candidate formal statements faster, which is really what deriving properties from specification means in practice. The properties are the formalization of the spec, not a separate step after it. So rather than thinking of it as spec first, then properties, then formal proof, it is more accurate to say the property set is the machine-readable spec, and formal is working on the spec once that translation has happened.”

Sometimes, specifications are purposely ambiguous. “Human designers interpret them with domain knowledge, prior experience, and the ability to ask clarifying questions,” says Southampton’s Davidmann. “AI models receive the specification text and generate output without the ability to flag ambiguity or identify inconsistency. Specification ambiguity is likely a significant contributor to LLM-generated code failures, but the current research literature does not yet systematically characterize how often this is the root cause, as distinct from model capability limits. The next step is developing methods for automated specification analysis that can identify ambiguity before it enters the generation pipeline.”

Should the problem be looked at the other way around? “Rather than having formal work on specs directly, there is a strong argument that modern spec authorship should be formal and machine-readable by construction,” says Arvind Srinivasan, design verification solutions engineer at Normal Computing. “This is the only way to solve the inherent problems of trust, coverage, and drift. This is structurally impossible using only existing formal methodologies, but is achievable if you can use novel solvers and languages like Lean.”

That can feed the long-term goal. “I want to give a spec to my large language model, and I want it to generate code,” says Paul Graykowski, director of product marketing at Cadence. “But how do you capture the true intent of what a spec is, and make sure that is what you’re using as your single source of truth? There are a lot of things that must be explored, things that existing specifications just take for granted.”

There is probably room for an iterative approach. “When you read RTL, it can give you some abstract information about what your RTL is trying to do,” says Synopsys’ Aneja. “It may not be perfect, but it can give you a good starting point, and then you can modify that spec in an incremental manner. You can go from there. It’s not perfect, but at least it gives you a reasonable starting point.”

Skills migration
One of the supposed advantages of auto-generated properties is that it would reduce the need for specialized verification people. This may not be the case.

“For teams without internal formal expertise, complex AI-generated formal properties can be a boondoggle to review and maintain, and there are well-understood boundaries to the utility of SystemVerilog assertion-based methodologies,” says Normal’s Srinivasan. “The key principle is internal consistency. How can heavily AI-driven design processes leverage formal as both a check against other AI-driven design and verification collateral, but also utilize other collateral as a check against spurious or incorrect formal properties? Users that place stable systems of record and internal consistency at the heart of their processes will be better placed to utilize these systems in a zero-trust fashion.”

Someone still must read each generated SVA property. “They need to judge whether the antecedent is too weak or too tight, whether the consequent captures the actual requirement, whether clocking and reset conditions are handled correctly, and whether the property could pass vacuously,” says Axiomise’s Darbari. “That requires fluency in temporal logic and assertion semantics, as well as deep understanding of micro-architecture. Without that skill, a team has no way to tell a strong property from a weak one that happens to look similar, and they will not know how to interpret a formal tool’s counterexample or a ‘proven’ result correctly either. So the practical requirement is that AI lowers the writing burden but raises the importance of having formal-literate engineers in the loop to interpret and validate the output. Organizations adopting this should budget for that expertise rather than assuming the tooling removes the need for it.”

There are some roles where formal properties may be more beneficial than others. “Formal verification is becoming a more important part of the solution,” says Ashley Stevens, director of product management and marketing at Arteris. “It is particularly strong for architectural compliance — ensuring ISA properties hold for all legal instruction sequences — and for enforcing correctness of hardware protocols in implementation verification. But formal is not a replacement for dynamic verification or system-level validation, especially when full SoC behavior and real workloads are involved. In practice, formal methods play a complementary role, proving deep corner-case correctness, while simulation and emulation establish end-to-end completeness.”

Problem areas
Vacuous assertions are a specific accuracy risk that deserves direct attention. “A vacuous assertion is an SVA that compiles correctly, passes the formal tool, and covers exactly nothing, because it is always true regardless of what the design does,” says Davidmann. “Vacuous assertions are not the same as correct assertions. A model that produces plausible-looking but vacuous SVAs provides false confidence while consuming formal tool capacity. A version of this technology that looks accurate on paper and is genuinely dangerous in practice is the one where the model is confident and wrong, the testbench was also generated by the model, and no one in the loop had the domain knowledge to notice. This is not a hypothetical failure mode. It is a workflow that is easy to construct inadvertently.”

There are significant costs associated with them. “In a formal verification flow, these errors are expensive,” says Cohen. “They consume tool runtime, engineer debug time, and — most critically — erode confidence in the verification results themselves.”

Formal verification involves multiple types of solvers, one of which is satisfiability modulo theories (SMTs). These look at determining whether a mathematical formula is satisfiable. “For agentic systems that put formal tools in the loop, there is a non-trivial cost from SMT solver runs,” says Srinivasan. “In addition, these scale with the complexity of the design and number of properties.”

Getting started
Deciding how to start using properties as part of a methodology is not obvious, and there are several issues that must be considered. There is also no single methodology that has been well tested, and it is likely that every company may need to work out what gives them the best balance of skills, time, and compute commitment, and the highest degree of verification closure.

AI needs to learn how generated properties are going to be used. “There are assertions for simulation and assertion for formal,” says Aneja. “There are techniques where you can write formal friendly properties, and that helps you with scaling in terms of, ‘Can you get a definite answer depending on how you’re writing the property?’ When you’re trying to write these properties, rather than writing a very long property, you want to divide that function into multiple smaller parts. That gives you scalability. Then you’re not getting stuck on a behavior that takes 200 cycles to do anything meaningful because it won’t work in formal.”

“Retrieval-Augmented Generation (RAG) offers a principled solution,” says Cohen. “Rather than relying solely on what an LLM learned during training, a RAG-enhanced system queries a curated knowledge base at generation time — retrieving the specific rules, patterns, and lessons that apply to the task at hand. RAG rules represent years of accumulated application knowledge — rules derived from real projects, real tool behaviors, and real failures. They encode not just what is syntactically correct, but what is verifiably sound; the difference between an assumption that constrains the environment appropriately and one that makes the formal proof space unreachable; between a property that checks the right behavior and one that passes vacuously; between timing diagrams that match the generated code and ones that silently diverge.”

There are stepped approaches that could be tried. “There is an intermediate step called formal test plan, where if you have a perfect spec, it talks about what your design does, not what you want to verify,” says Aneja. “The idea is that with all these LLMs and agents, you have the ability to read text, look at timing diagrams, look at FSM diagrams, other pictures you may have, and then you can extract certain features based on the designs you are doing. And you can train your system to say, is it a CPU design? Is it a GPU design? Is it an AI accelerator? Go one level down, is it a memory controller? Is it an interrupt controller? Is it a bus bridge? Or is it some interconnect across different managers and subordinates? Depending on what that is, it can extract certain features that you may want to test.”

The same considerations go for choosing an LLM. “Domain boundary awareness needs to become a first-class engineering discipline,” says Davidmann. “Before adopting any AI model into a production flow, the right question is not only how accurate the model is, but what it was trained on, what that distribution does not cover, and how close the actual design is to that boundary. Every team deploying these tools should run a deliberate boundary-probing exercise on a representative sample of their most complex and novel design patterns, verifying the outputs independently against what a domain expert would produce. That exercise identifies where the distribution ends and the model uncertainty begins. Without it, deployment is proceeding without the information needed to manage the risk.”

Start small and build confidence. “Pilot on a bounded, well-understood block first, compare the AI output against an existing hand-written property set, and measure the gap before rolling this out broadly,” says Darbari. “Finally, this only works well alongside engineers who already understand formal methods. It is not a way to skip that expertise. It is a way to make expert engineers faster. This is one area where I’m seeing an interesting demand from bigger design houses. Management wants engineers trained in formal so they can drive the entire ecosystem of tools and apply methodology properly.”

It is also important that you consider the domain in which you are working. “Tooling is currently ahead of the governance,” says Davidmann. “Most teams do not yet have a standard for documenting which assertions are human-authored, and which are AI-generated, or what that distinction means for sign-off confidence. In addition, most vendor documentation does not specify the training scope, failure modes, or domain boundaries of the models being deployed. Both gaps need to close before AI-generated content scales into safety-critical designs.”