Technology is truly useful only when it can improve existing methodologies. Attribute generation is still working towards this goal, and in the long run, it could be of great value.

Key points:

• The top-down semiconductor development process has always been the goal of chip design, and "left-shifting" is making this goal increasingly achievable. The problem lies in the starting point – the specification details – which are often incomplete or simply non-existent, due to the chip industry's long-standing poor performance in writing specifications.
• AI can be integrated into existing processes in various ways. However, the ability to do so does not necessarily mean that it is the right thing to do. This is one of the major challenges faced when implementing AI. Many existing tasks can be completed more efficiently through proxy-based processes, but it is not clear whether this is indeed the best approach.
• When AI begins to help address the area that has always been weak in the past—creating high-quality, complete specifications—this limitation becomes particularly evident. The real question is whether AI can enable the design or verification environment to automatically derive from the specifications. Perhaps a more accurate goal is: whether AI can help create better specifications. With better specifications, downstream design will be much easier.

“AI can generate a SystemVerilog assertion in just a few seconds,” said Ben Cohen, an expert in verification technology and author of books. “But whether this assertion is meaningful depends entirely on what it is generated from, and in practice, this source is rarely a single, clear, natural language specification. It is often just a vague paragraph that needs to be clarified before it can be trusted.”

Solving this issue should be regarded as a high priority. "The increasing complexity of modern SoC design has led to the convergence of AI-assisted artifact generation and verification, which has shifted from a research option to a practical necessity," said Simon Davidmann, a researcher at the AI and EDA departments at the University of Southampton. "The verification issues have become so significant in practice that they cannot be addressed without AI assistance. A ratio of 5 verification engineers to 1 design engineer in processor development is not an exception in labor planning; rather, it is a sign that the complexity has surpassed the capabilities of existing methods."

From specifications to any actual results, it's still not a reality today. “If we really want to make this a reality, we need to be more disciplined in writing the specifications,” said Ravindra Aneja, the Application Engineering Director of Synopsys. “If we truly want it to become a reality, we must take action. As an industry, are we ready? No, I don’t think we have reached that stage yet. I don’t believe we have reached a point where, whether starting a new design or working on a derivative design, we can say that the specifications are good enough.”

Are we even thinking about this issue from the right perspective? “A prose-style specification document cannot be directly inferred by formalization tools, as formalization engines deal with precise, unambiguous statements that can be machine-checked, not natural language,” said Ashish Darbari, CEO of Axiomise. “What AI can do is to help bridge this gap by converting prose into candidate formalized statements more quickly, which is essentially deriving the meaning of attributes from the specifications. Attributes are the formalized expression of the specifications, not an independent step that follows that. Therefore, rather than thinking of it as specifying first, then attributing, and then formally proving, it is more accurate to say that the set of attributes is the machine-readable specification, and formalization is the process of working on the specification after this step of translation is completed.”

Sometimes, the specifications themselves are intentionally vague. “Human designers interpret them by combining domain knowledge, past experience, and the ability to raise clarifying questions,” says Davidmann. “The AI model, on the other hand, generates output directly after receiving the specification text, but it lacks the capability to identify ambiguities or inconsistencies. Specification ambiguities are likely one of the important reasons for code generation failures by LLM, but existing research literature has not systematically characterized to what extent they are the root cause, rather than just limitations in the model’s capabilities. The next step should be to develop automated specification analysis methods to identify these ambiguities before they enter the generation process.”

Should we look at this issue from the opposite perspective? "Rather than letting formalization directly affect specifications, there are good reasons to believe that modern specification writing itself should be formalized and machine-readable from a structural standpoint," says BJW_KEEP_00001, Design Verification Solutions Engineer. "This is the only way to address inherent problems like trust, coverage, and drift. This isn't structurally possible with existing formal methods, but it's possible with new solvers and languages like BJW_KEEP_00003."

This can serve a long-term goal. “I want to hand over the specifications to my large language model and then have it generate the code,” said Paul Graykowski, the product marketing director of Cadence. “But how do you capture the true intention of those specifications and ensure that they are the only source of facts you use? There are still many things that need to be explored; many existing specifications take these things for granted.”

Perhaps an iterative approach can be adopted. “When you read RTL, it can provide you with some abstract information about what RTL aims to achieve,” said the Aneja of Synopsys. “It may not be perfect, but it can give you a good starting point, and then you can gradually modify that specification. From there, you can continue. It’s not perfect, but at least it provides you with a reasonable starting point.”

Skill Migration

One advantage of automatically generated attributes is that it may reduce the need for specialized verification personnel. However, this may not necessarily be the case.

"For teams without internal formalization experience, generating formalized attributes for complex AI can become a cumbersome burden that is difficult to review and maintain. Moreover, the practicality limits of SystemVerilog assertion methods are well-known," said the Srinivasan of Normal. "The key principle is internal consistency. In a design process that relies heavily on AI, how can we use formalization not only as a check on other AI-driven design and verification materials, but also leverage those materials to detect false or incorrect formalized attributes? Users who place stable system records and internal consistency at the core of their processes are better suited to using such systems in a zero-trust manner."

There is still a need for someone to read each generated SVA attribute one by one. "They need to determine whether the antecedent is too weak or too strong, whether the consequent truly captures the actual requirements, whether the timing and reset conditions are handled correctly, and whether the attribute might be vacuously valid," says Darbari of Axiomise. "This requires an understanding of both temporal logic and the semantics of assertions, as well as a deep knowledge of microarchitecture. Without such capabilities, teams cannot distinguish between a strong attribute and one that may seem strong but is actually weak, nor can they correctly interpret counterexamples or 'proven' results from formalization tools. Therefore, in reality, while AI can reduce the writing burden, it highlights the importance of having engineers who understand formal methods in the process to interpret and verify the outputs. Organizations that adopt such tools should budget for this specialized skill, rather than assuming that the tools will eliminate the need for it."

In certain roles, formalized properties may be more valuable than in others. “Formal verification is becoming an increasingly important part of solutions,” said Arteris, the Product Management and Marketing Director of Ashley Stevens. “It is particularly powerful in terms of architectural compliance—ensuring that ISA properties hold true for all valid instruction sequences—and it is also suitable for enforcing the correctness of hardware protocols during implementation verification. However, formalization cannot replace dynamic verification or system-level verification, especially when it comes to complete SoC behaviors and real workloads. In practice, formal methods play a complementary role: they prove the correctness of deep boundary conditions, while simulation and simulation acceleration establish end-to-end integrity.”

Problem area

Empty assertions are a specific type of accuracy risk that requires direct attention. “An empty assertion is a kind of SVA; it can compile correctly and pass formalization tools, but in reality, it covers nothing at all, because no matter what the design does, it is always true,” says Davidmann. “An empty assertion is not equivalent to a correct assertion. A model that can generate something that looks reasonable but is actually empty will consume the capabilities of formalization tools while creating false confidence. That kind of version, which seems accurate on paper but is extremely dangerous in practice, is both confident in its model and incorrect. The testing platform is also generated by the model, and no one in the process has sufficient domain knowledge to identify the issues. This is not a failure mode in theory; it’s a workflow that can easily be constructed unintentionally.”

The cost of such errors is high. “In the formal verification process, these errors are very costly,” says Cohen. “They consume tool running time, engineer debugging time, and most importantly, they erode people’s confidence in the verification results themselves.”

Formal verification involves various solvers, one of which is the model theory satisfiability solver ( SMT ). They are used to determine whether a mathematical formula is satisfiable. "For proxy systems that incorporate formal tools into their processes, running the SMT solver incurs costs that cannot be ignored," says Srinivasan, "and these costs increase with the complexity of the design and the number of properties."

How to get started

Deciding how to incorporate attributes as part of a methodology is not easy; it requires considering multiple issues. There is no single, fully validated methodology, so it is likely that each company will need to explore on their own to find the best balance between skill investment, time commitment, computational power, and the degree of validation achieved.

AI needs to learn how the attributes they generate will be used. "There are assertions for simulation, as well as assertions for formalization," says Aneja. "There are some techniques that allow you to write attributes that are more suitable for formalization, which will help you make progress in scalability. That is, 'can you get a clear answer based on how the attributes are written?' When you try to write these attributes, instead of writing one long attribute, it's better to break down that function into multiple smaller parts. This is more scalable. Then you won't get stuck in a scenario where meaningful behavior doesn't occur until after 200 cycles, because that doesn't work in terms of formalization."

"Retrieval-enhanced generation (RAG) provides a principled solution," says Cohen. "Rather than relying entirely on what is learned during LLM training, it's better to have a system with enhanced RAG query a filtered knowledge base during generation – retrieving specific rules, patterns, and lessons learned related to the current task. The RAG rules represent years of accumulated application knowledge; these rules come from real projects, real tool behaviors, and real failures. They encode not only content that is grammatically correct, but also content that can be verified as correct; they include whether a assumption appropriately constrains the environment or makes the formal proof space inaccessible; they include whether a property checks correct behavior or merely passes through vacuously; they include whether a timing diagram is consistent with the generated code or deviates silently."

You can also try a phased approach. “There’s an intermediate step called the formal test plan, which involves having a perfect set of specifications that describe what your design is supposed to do, rather than what you want to verify,” says Aneja. “What I mean is, with the help of these LLM and proxies, you can read text, view timing diagrams, examine FSM diagrams, as well as any other images you may have, and then extract certain features based on the design you’re working on. You can train the system to determine: Is this a CPU design? Is this a GPU design? Is this a AI accelerator? Moving on to the next level, is it a memory controller? An interrupt controller? A bus bridge? Or some kind of interconnection between different master and slave devices? Based on this information, it can extract certain features that you might want to test.”

The same considerations apply when choosing LLM. "Domain boundary awareness needs to become a primary engineering discipline," says Davidmann. "Before introducing any AI model into the production process, the important questions are not only how accurate the model is, but also what it has been trained on, what distributions it does not cover, and how close the actual design is to those boundaries. Every team that deploys these tools should consciously conduct boundary detection on a set of representative, most complex, and most innovative design patterns, and have domain experts independently verify the results. This practice can identify the endpoints of the distribution and the starting points of model uncertainty. Without it, deployment is proceeding in the absence of the information needed to manage risks."

Start with small steps to build confidence. “First, pilot in a module with clear boundaries and thorough understanding. Compare the AI output with the existing manually written set of attributes, and measure the gaps before widespread implementation,” says Darbari. “Ultimately, this will only be effective when used in conjunction with engineers who already understand formal methods. It’s not meant to bypass such professional capabilities, but to enable expert engineers to work more efficiently. In this regard, I’ve noticed an interesting demand from large design companies. Management wants engineers to receive formal training so that they can drive the entire tool ecosystem and apply methodologies correctly.”

At the same time, it is also important to consider the field you are in. “Current tools are already ahead of governance,” says Davidmann, “Most teams still do not have standards to record which assertions are manually written and which are generated by AI, or what this distinction means for the confidence in verification. In addition, most supplier documents do not explain the training scope of the models, failure modes, or the domain boundaries for deploying the models. These two gaps need to be filled before the content generated by AI extends to security-critical designs.”