The Future For Formal Verification

Experts at the table: Semiconductor Engineering sat down to discuss possible future directions for formal verification technology with Ashish Darbari, CEO for Axiomise; Jin Zhang, product management group director for the Verification Group at Cadence; Sean Safarpour, executive director for R&D at Synopsys; and Jeremy Levitt, principal engineer for Digital Verification Technology at Siemens. What follows are excerpts from that discussion. Part 1 of this discussion is here, and Part 2 is here.

L-R: Axiomise’s Darbari; Cadence’s Zhang; Synopsys’ Safarpour; and Siemens’ Levitt.

SE: Does formal have a responsibility to the whole verification process, because the perfect set of properties is the specification of what you’re trying to design? Today, verification engineers translate from specifications written in loose English language most of the time, and try to convert that into properties. Should we turn the problem on its head and start defining these things using formal specifications? Maybe formal tools are not able to prove all of them, and that carves out what DV needs to go off and tackle.

Darbari: That would be the holy grail. That would be the best legacy of generative AI, if it can get us to a machine-readable specification for the entire chip. I would say it’s possible, and it is highly likely that we can get to that point. This would allow people to get more assertions, and by that, I mean SystemVerilog properties to be used as formal checks on the interfaces, or as guides for UVM testbenches. But most companies that understand the value of good specifications invest in interface specifications as their starting point. So clearly, there is value in creating a machine-readable spec. Some of the bugs we see, which are very insightful, are just because of the complexity of interactions. There are so many different things happening, and architects and designers often have not considered certain behaviors. And that is the beauty of formal. It’s forcing you to consider the entire space of interactions. Designs are massively complicated these days. There are just so many things happening. But if we can do all of the difficult or boring work easily through machines, then we can focus our brains on the smart things better.

Safarpour: We are definitely on the right track, both with agentic flows that we demonstrated at DAC with Marvell, and with RAG capability. If I look back a year, what we could generate was really Mickey Mouse stuff. You’d be looking at one-line properties, and anytime you want to go beyond that, things would break down. But now we’re consistently generating medium complexity properties correctly in our agentic flow. What is missing is the really hard end-to-end stuff that needs complex auxiliary logic, maybe hundreds of lines in an always block. Those things are going to be a challenge. But it’s all about the patterns. Once we start capturing the necessary design patterns, we’ll do better. On the generation side, we’ll get there. I don’t think we’re going to end up going down to a formalized specification that is machine-readable. It is more likely to be the opposite. We’re going to go more into natural language. But I already see our customers are putting more emphasis on the specs and the test plans than they had before. Now they see that as the entry point, whereas before when you would ask people, ‘Do you have a spec for this,’ they would laugh you out of the room. They might say, ‘We have a spec, but it’s way outdated. Look at this section. But we changed something, so it’s not quite accurate.’ Now they understand they have to do better, not just for formal, but also for design creation. There’s a lot of stuff happening on that side, as well, that this is going to be the single-entry point. And then there’s going to be all sorts of LLMs and automation and high-level synthesis and other things coming into that picture. Its importance is growing, but more toward the natural language side of things than a machine-readable spec.

Zhang: Natural language communication is where we’re going. I know there’s a lot of ambiguity in how we express English, but that’s the power of LLMs — being able to tell the subtle differences or interpret it differently, to see which one is really what you wanted. I don’t know if people are willing to learn yet another formalized way of expressing things, but a lot of effort has gone into taking in the spec and generating a test plan from it, generating the testbench. We have been working on a spec miner, taking your specification, trying to bring that down to the rest of the flow, driven by spec, but not necessarily a formal spec. Right now, people are still working on having a good spec. Hopefully that will change.

Levitt: The ideal objective would be to have an SVA description of your specification, which everyone agrees is correct, but no one’s going to pick SVA. You’re going to want it in the natural language description, and that’s always going to be the reference. When something goes wrong, people will ask, ‘What does the natural language description say?’ And if that’s out of sync with the SVA, then one or the other gets fixed. But it’s hard to see how users would turn to SVA as their spec.

SE: Even if it is in a natural language, won’t it fall on formal technology to say that your specification is inconsistent, or your specification has holes, or to point you to what it takes to complete the specification in an unambiguous manner?

Levitt: LLMs can certainly help by taking that natural language specification and turning it into SVA properties, and then perhaps comparing that against your actual set of SVA properties, which you believe captures that spec. LLMs have a big role to play there, making sure that your natural language specification is captured by your SVA specification. Today, that is discovered through trial and error. And writing designs, people notice holes. But with LLMs, you can be much more proactive to make sure that the natural language is consistent with the SVA set, which you believe captures the same requirements.

Darbari: Whatever synthesis is done on the specification documents, written in whatever language they are written — it could be Japanese, it could be English — the end result should be a machine-readable spec that can be used for formal and simulation, and potentially emulation, as well. That would be a way to resolve the ambiguities. They would be minimized if you compare the new and the old SVA. But unless they are tied back to the requirements, at least for some chips, if you don’t make them join up, there’s still a gap between what was coded and what was written in a given language.

SE: It sounds like you are both describing a meeting in the middle approach.

Levitt: Many protocols already have SVAs that people use, and they believe they capture the protocol. So to clean that up, LLMs can go and generate what they think are the set of SVA properties, and then you compare the two sets and try to find holes. If you’re starting with a brand-new protocol, maybe the place to start is with the LLMs, and have that as your starting point. But often you already have a set of SVA properties that capture the spec. If you want to clean those up, this is a starting point for LLMs.

Safarpour: On the design side, LLMs are already being used a lot. We see some folks using it more as a copilot, helping them generate chunks of code. If we look at what’s happening on the software side, more and more code is being automatically generated by these LLMs or copilots. The same thing will be happening on the design side. This is quite interesting for formal. This is where formal and completeness — the exhaustiveness of formal — can play a very unique role. The stuff that the LLMs will generate is based on patterns, statistics. Formal is definitive, as long as we are careful in the methodology that we use — just like we had to deploy when we introduced synthesis. You don’t want to use the same company to do equivalence checking to verify what the synthesis tool came up with, or the same algorithm, or front-end stuff. As long as you’re aware that you need a methodology where the generation and the verification path are separated, formal is going to play a really big role there, making sure that what you want to be generated actually got generated and is correct. The functionality is correct, and all the other metrics that will be important to the end user. This will be more important for formal than many other technologies, like simulation and emulation.

SE: In many parts of the EDA flow today, we hear about them becoming vector-dependent. Power, timing, even reliability — all of these things are vector-dependent. It seems as though a lot of people are struggling with this because they don’t know what a realistic, worst-case scenario will look like. A number of you have mentioned that formal is helping people find the cases they didn’t consider, and we have seen formal used for generating test cases for functionality. Could formal methodologies be used to help in some of these other processes, where you’re perhaps trying to find the worst-case conditions, or a case when the maximum number of cores in a system are being used? How much can formal help with some of these other problems?

Darbari: We have been using formal a lot for this work. Some of it is through automation, using Apps, but also during formal property verification (FPV) where we are addressing performance analysis in a number of cases. It is still very early days, because people are not used to seeing formal being used in that way. People are quite surprised when we mention that this is possible. Then the question turns to metrics, and how do you quantify this at the system level, which I don’t currently know the answer to. We certainly can produce cases that show that if these conditions were to manifest in silicon, it would have a performance impact. From an automation point of view, security is another nice area where there is an application of formal, because it’s an area of addressing unknowns. Formal is very good at finding unknown unknowns. It’s a natural fit. The EDA guys have also been building Apps that address multiple applications.

Safarpour: Security is an obvious one, but other examples are that they know the preconditions for things that they want to check. They may still be in the functional domain, but they know they want to explore things when their FIFO is almost full. And then they want to make sure there’s an exception thrown over here, so you can set up these conditions for what we still see as a functional domain. These may give you very interesting simulation vectors, or just vectors in general. They demonstrate how to hit some of these cases that, maybe from a performance point of view, may be interesting. The other one that we do quite often is to come up with different scenarios that maximize toggle count, the number of transitions, and things you want to see. Obviously, you could come up with cases with formal where everything could be toggling and your chip might burn, but that might not be something that would happen in reality, because you have a lot of guardrails and things like that in place. Or, if you adhere to the protocol, those conditions are not going to happen. But it’s as easy as writing FPV-type properties for these things. SVA is very expressive. And if somebody knows what they’re after, what they want to do, they can do that. I don’t know if a lot of our customers do that, but the capabilities are there in the tools, and they could express it.

Zhang: Besides just looking at using SVA to do verification, there’s the power of equivalence checking — formal equivalence checking. This is when you want to do some PPA optimization, you want to make sure the functionality hasn’t changed. That type of application, or any retiming, or any enhancements for your design — the derivatives, leveraging formal under the hood to make sure that the functionality hasn’t changed — is a widely used application already. And talking about security, I know there are companies using the counterexample from formal verification as vulnerability scenarios to see if this will introduce any vulnerability in the design. There are definitely creative applications of formal to connect to the other processes in the flow.

Levitt: Some additional applications are FuSa-related. There are a lot of opportunities for formal in the functional safety space to come in and verify that your design meets FuSa requirements. How do you simplify your design? Another area is power, with clock gating. Another area is X checking. Do I really need to reset all these registers? Can I simplify my reset sequence and take reset off a bunch of registers and reduce power? There are many interesting areas for formal to be applied outside of just purely functional verification. If you can describe what you’re looking for, formal can find it. This is much more powerful than anything you can do with simulation.