chipx.cam

Key Takeaways:

• Turning a specification into a set of properties is something that LLMs as capable of doing. However, most specifications are inadequate, AI tools are immature, and a large amount of human intervention is required.
• There are hidden dangers in blindly accepting the output of AI tools. Other methods must be used to assess completeness.
• The ROI is not clear. While a greater number of properties can be generated, the human cost of verifying them will see a significant increase.

One of the biggest problems for formal verification has always been the difficulty associated with writing properties. While language standards have been in place for a couple of decades and tools have improved dramatically, that roadblock has never been cleared — perhaps until now, thanks to AI. AI is known for its ability to read a natural language document and synthesize information from it. One application with high utility would be the ability to read a specification and to automatically create a set of properties that could be used to verify if an implementation matches the specification. However, several challenges exist, and a number of pitfalls await those who do not fully understand the hazards. One portion of the SystemVerilog language enables properties of a design to be formally defined. When these properties are used within a verification environment, they are referred to as assertions. Properties define logical and temporal relationships between signals, enabling protocols and other things to be explicitly defined. A set of properties should be able to define the complete set of behaviors intended in a design and to do that without being entangled with how those behaviors are realized. In that respect, they represent a specification against which an RTL implementation can be judged for correctness. But the SystemVerilogAssertion (SVA) language is not easy to learn, especially given that it is declarative in nature, rather than the object-oriented procedural nature of languages used in most parts of the design and verification flow. For many years, the industry has attempted to create tools and methodologies that make their creation simpler. Recently, LLM-based tools have started to make significant headway even though there are several breakthroughs that still need to be made. One recent breakthrough is the creation of knowledge graphs, which are defined by Cohen and Chibani [1]. “A knowledge graph stores information as a network of things and the relationships between them, rather than as flat text. It has three parts: nodes (the entities — a signal, a module, a requirement, a port); edges (the relationships — drives, resets, responds-to, belongs-to); and triples, the storage unit, written as (subject → relationship → object).” KGs act as a database of information that can be quickly accessed, rather than relying on the LLM to extract it every time it’s needed. “Ordinary RAG retrieves chunks of text that look relevant; a KG retrieves specific facts and their connections. That is why the KG-based frameworks argue they give better grounding — there is less chance the model invents a signal name or misreads a relationship, because the relationships are stored explicitly. [1]” Ironically, one big problem is finding an adequate specification. “The ideal is that you have a perfect spec, but that has not existed at least in the last 30 years,” says Ravindra Aneja, director of applications engineering at Synopsys. “The majority of the time there will not be a perfect spec. In fact, you may not have any spec at all. This may depend on whether it is a new design or a derivative design, who is writing it, and which organization. But until AI came along, the notion of having a perfect spec or documentation was not the coolest thing to do in the world. People often start designing before they fill in the spec because they already have some ideas about what they want to do. With the advent of AI, people are paying more attention.” A significant amount can be accomplished today. “AI can read a spec document, a protocol standard, or even RTL comments and propose a first pass of assertions covering resets, handshakes, one-hot conditions, and obvious safety checks,” says Ashish Darbari, CEO of Axiomise. “This is possible when the specifications are on standards that do not change frequently. That draft speeds up the tedious part of writing boilerplate SVA.” The desire to do this has existed for some time. “People claim that reading a specification and converting it into some other tangible artifact is something that AI is well suited to solve,” says Abhi Kolpekwa, senior vice-president and general manager at Siemens EDA. “It also needs an aspect of change management, because the spec is likely to change. For a verification flow to have change management, there is a lot more that needs to happen outside of agents. This is called contextual intelligence. We need the ability to create a context and contextual intelligence that not only understands the changes, but also makes more informed decisions considering the history and a possible future in the given verification flow context.” Specifications are never fixed. “I’m in the process of figuring out the spec and I’m doing the development, but marketing then wants this additional feature, and you go back and modify the spec,” says Synopsys’ Aneja. “Sometimes that deviation could be minor. Sometimes it could be major. Whatever changes you are making, how would it reflect in your design and in your verification environment? AI is pretty good at this, figuring out what the deviation is and how it is going to impact your verification. There’s a lot of discussion in the industry about how you can manage this change-based design process. This is where AI is going to be very useful.” Danger ahead
Was that specification complete? “Completeness is a different question entirely,” says Axiomise’s Darbari. “Most real-life silicon development does not happen in isolation. And even when projects are entirely new, it is rare that complete specifications would be written capturing all micro-architecture and architecture, including interfaces where typically most bugs reside. In my experience, AI-generated property sets are strong on structural and syntactic coverage and weak on architectural intent, and the ‘why’ behind a rule. So usefulness is real, but completeness has to be established independently, usually by an engineer who understands the design intent well enough to know what is missing.” Was all information used? “How useful and complete those assertions are depends on how good your AI engine is, and how accurately it understands the nuances of the specifications,” says Yaron Ilani, design verification solutions engineer at Normal Computing. “At Normal, we tackle this challenge by running ‘auto formalization’ and generating an ontology. The risks could be wrong assumptions resulting from gaps or ambiguity in the specifications. These risks could be mitigated by running a preliminary step of spec auditing.” Both problems can result in an incomplete set of properties. “The biggest danger is false confidence,” says Darbari. “A team gets a large batch of properties, runs them through a formal tool, sees green proofs, and treats that as sign-off. But a proof is only as good as the property, and a weak or vacuous property proves trivially without checking anything meaningful. AI-generated properties are particularly prone to this because a model can produce syntactically valid SVA that is logically too permissive, missing or over-constraining an antecedent, or checking the wrong signal relationship — and it will still compile and pass.” That ends up being a verification task itself. “Deriving properties from a spec requires distilling unstructured and multimodal information into provable statements,” says Hanna Yip, product manager lead at Normal. “While the extraction process itself can be efficient, it can be quite challenging to ensure what’s extracted is correct.” In the past, verification happened when the design team interpreted the specification, the verification team interpreted the specification, and then those interpretations were verified against each other. Sometimes that identified a problem with the specification itself. “Generated properties can quietly encode the AI’s own misreading of the spec as if it were ground truth,” says Darbari. “Errors in interpretation get baked into what looks like a rigorous artifact. There is also a scale risk. If these properties feed downstream FMEDA, safety cases, or certification evidence for ISO 26262 or ISO 21434, an unnoticed gap does not stay contained to one project.” It quietly means that you cannot trust what AI has done. “Trust is a big issue,” says Kaye Mao, product design lead at Normal. “How do you verify work that you did not do, especially when agents are hyper-confident in their correctness and trained to pass the sniff test? For example, how do you verify a test is actually testing the design as outlined in the spec? Do you have to look at the actual waveforms? That itself is time-consuming, so it may require novel ways of checking agent work.” Given recent incidents with AI going rogue, Mao adds another potential concern. “Another danger is failing to limit what collateral the agent can access for a given task. Agents will always cheat if possible. For example, they may use the design to generate test cases, which defeats the point of keeping verification and design separate.” ROI
While it is clear that AI is capable of doing some aspects of the task, it also has costs and creates new work. Does it add up to a significant gain? “I’m increasingly noticing that silicon design houses — even the ones who are building AI hardware powering the agents — are getting nervous about unreasonable use of agentic AI in particular by junior engineers and people who are quick to claim they are experts without the hands-on experience,” says Darbari. “It is efficient at the front end, but it can be inefficient at the back end if teams are not careful.” This may improve over time. “It depends on how big the spec is,” says Normal’s Kao. “More philosophically, if we define efficiency as saving engineers time, it’s unclear, given the new tasks of verifying agent output, how much actual engineering-time efficiency we see today. I expect efficiency gains to improve as models get better and we devise better ways of verifying agent work.” There are several ways this can be measured. “Complexity scaling is not strictly computational,” says Arvind Srinivasan, head of solution architect at Normal. “There’s a human efficiency associated with data completeness and review. As with handwritten properties, simple, well-documented parts of a spec are easier to cover than more sophisticated parts of the design. To enable sublinear scaling of formal coverage in modern designs, there is a need to augment existing formal tooling with AI-native formal tooling and alternative, non-SVA autoformalization strategies.” Scaling has always been an important aspect when formal solvers are used. “There are a lot of techniques in the formal world, which helps you scale,” says Aneja. “The good news is that in the past we had to train junior engineers about these techniques. Now you can provide that knowledge base within these agents, and when they write the property, they can become very efficient in writing those formal properties. That will give you better answers, much faster answers. You’ll be able to do more in the same amount of time. It helps you in scalability.” Human in the loop
All agentic flows need a human in the loop today. “Drafting hundreds of candidate properties that used to take days of manual reading now takes minutes, and that is a genuine productivity gain,” says Darbari. “Where the efficiency can evaporate is in review. If every generated property or debug waveform needs the same depth of scrutiny as a manually generated one, and the volume has gone up tenfold, the review burden can outpace the drafting savings.” Someone has to review it. “You can’t just take it as it is because otherwise you’ll be shooting yourself in the foot,” says Aneja. “LLMs can do a lot of interesting stuff, but they can also fool you. That’s the reality of life. It can give you a lot of automation, provide a lot of efficiency and productivity, but someone who knows that design will have to review it manually, tweak it, guide it, and you keep accumulating that information. Over time, you may be able to train it or get to a point where it can do a pretty reasonable job out of the box.” There are many ways that LLMs can fool you. “Vacuity checking, coverage analysis, and cross-checking against the spec still have to happen, and those steps do not get faster just because generation did,” says Darbari. “They should run vacuity and coverage checks as standard practice, not as an afterthought, because generated sets are more likely to contain trivially true properties than carefully hand-crafted ones.” But this still creates a problem. “People want to stay in control, because they’re held accountable for the consequences,” says Mao. “It seems unrealistic to expect folks to understand formal. Rather, what other representations can be used to verify the accuracy of a formal representation of a spec? Is it waveforms? Is it something else?” Standard practices need to be built into the flow. “Treat AI-generated properties as a draft, never as an accepted deliverable,” recommends Darbari. “Build a review gate into the flow before anything reaches a regression suite. Users should insist on provenance — which spec section, which requirement, or which RTL construct produced each property — so reviewers can trace back and check the mapping.” If trust is built, the gains get larger. “This is good news for DV engineers looking to get into formal verification or assertion-based simulation,” says Normal’s Ilani. “For many years, we used to joke that writing effective formal properties requires a PhD. Now, AI-driven flows lower the barrier to entry for DV engineers looking to run formal verification. Part of this new methodology, in my opinion, is to leverage agentic flows and make them your wingman, your PhD in formal verification assistant, to help you not only understand your formal testbench, but also run it, debug failures, and propose solutions.” Reference
1. RAG-SVA in the Landscape of LLM-Based Assertion Generation, Cohen and Chibani [Editor’s Note. Part two will dig deeper into the team skills required and the best ways to introduce those into a methodology. It will explore whether this will enable raising the level of abstraction.] Related Articles
The Impact Of AI Automation On Chip Design
Change is coming, but how quickly depends on the availability of data and when chipmakers are confident enough to let AI take over. Rethinking Chip Verification
Specification engineering is gaining traction as a potential solution to the verification bottleneck. Does Your RISC-V Core Meet The Standard?
Verifying an extensible processor is more than a one-step process, especially when software compatibility is important. The post From Spec To Formal Properties appeared first on Semiconductor Engineering.

Source: https://semiengineering.com/from-spec-t ... roperties/