Advances In Formal Verification Technology

Experts at the table: Semiconductor Engineering sat down to discuss advances in formal verification tools and methodologies 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 EDA. What follows are excerpts from that discussion. [Part 2 of this discussion is here.]

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

SE: We hear a lot about advancements in formal verification when there is a startup, but less so when the development is happening within the large EDA companies. What technological advances are being made here?

Levitt: These are exponential problems, so there’s plenty of headroom to improve performance. There have been points where there have been discontinuities, and new algorithms have come along. But even without that, from release to release, from year to year, you see the tools get 25% faster to twice as fast. We see exponential performance gains. Of course, designs keep getting bigger, and it is a very difficult game of chase you’re playing here. But there is significant improvement in the performance of the tools. That is sometimes due to tuning of heuristics, applying machine learning to figure out better parameter settings, or better areas of investigation. It is due in part to the use of clouds, where there are extra compute resources available, and that allows you to do many things in parallel. And we’re beginning to see some improvements from the application of LLMs, but that is maybe more in the future than it is in the tools today.

Safarpour: Startups do make a lot of noise. We haven’t had a startup in the pure formal verification domain for a while. The folks using formal are seeing a lot of innovation, a lot of impact, and an expansion in the types of problems that they can solve. The profile of who uses formal verification has changed dramatically. A lot of these companies are showing that formal verification can add a lot of value in terms of finding bugs and doing sign-off. I want to talk about the SAT competition. SAT solvers are one of the main foundation solvers for formal verification, and the SAT competition has been around for about 20 years. Every once in a while, a new SAT solver comes up. There was Chaff and zChaff. This was groundbreaking, and people said this is probably as good as it gets for an NP-complete problem. And then MiniSAT comes up. These things happen, and then for a while, even SAT experts would say things quieted down. But if you go back five years, kissat, MapleSAT, a lot of new solvers are coming. If you look at the SAT competition and the recent results, they’re just blowing the previous year’s results out of the water. There’s still a lot of innovation happening, from the fundamental level of the solvers all the way up the application chain. There’s still a lot of innovation happening even at this basic level. Some of the latest data is also showing how AI can help improve a lot of these SAT solver algorithms. It’s pretty exciting, and there’s a lot of movement. For people a little bit outside of the community, it’s hard to see, but I think it’s a very exciting time to be in this area.

Zhang: Jasper [owned by Cadence] is still very successful in the market. Everyone’s efforts are keeping the R&D team on their toes in developing new technologies. A lot of those are behind the scenes at the engine level. These are improvements that users may not see. Our ideal goal is not to give them a lot of knobs for them to tune, but rather to give them orchestration so that it’s easier for them to use formal. That has been the biggest challenge over the years. Technology improvement, SAT solvers and cloud, distributed computing — all of those things are happening. A lot of investment has gone into it from all companies, just to stay on par or ahead of the competition.

Darbari: All of the EDA companies are producing wonderful tools, which have made people like us look bright in the field. A lot of the work that has been done recently is in SAT solvers. As users of formal tools, we see them making a big difference in the proof convergence rate. But let me take a step back and describe five key areas that define formal usage. The first one is property generation. Who writes the properties, and how good are these? They’re not going to be invented in the ether unless they are standard protocols. If they’re tied to specifications, then the elephant in the room question is, ‘How do you take complex, large specifications and turn them into meaningful properties?’ Unless you have that, you can’t actually solve the functional verification problem with formal, although a lot of app-driven formal continues to be used and is making a big difference. Unless we start to adopt formal in a functional space by making better connections with specifications, and making property generation faster, better and more efficient, we can’t actually make that much of a difference with formal. With efficiency comes another associated challenge, which is constraint refinement and making sure the constraints are captured correctly and we have them modeled efficiently. Once these two things are done — as in, assertions are written and assumptions are adequately modeled for correctness and efficiency — then if they fail, you have the third challenge, which is debug. A lot of things have been happening in the tools. And then you want to talk about the next elephant in the room, which is proof convergence. How do we make those things better and faster? Design complexity keeps increasing several-fold, so there’s always a catch-up to do. But then sign-off and coverage, and how do you holistically address all of the last bits of the story to make sure everything that was formally verified was actually done properly, that no bugs were left in the silicon and so on. From a user point of view, the shift is moving toward customization of the solution layer. This is where we are doing a lot of work, as well. Customers are now seeing formal in a way they were not perceiving it before. If you’re talking about RISC-V, for example, there is a lot of custom solution work that we have done. We are finding benefits in this. Ten years ago, if you went to somebody and said you could verify an in-order processor or an out-of-order processor exhaustively with formal, they would laugh at you. That was not something they could think of. But today we can do this. It’s a combination of solvers and the application engineers writing the properties effectively. A lot of formal is quietly making a difference in various aspects of verification. I’ve only talked about functional, but there are other aspects where it’s making a huge impact.

Jeremy: My first answer was about the performance of the engines, which definitely have been increasing exponentially. But Ashish brings up an excellent point about the improved use models and how easily the tools allow users to access this power. We have seen continual innovation there on the tool side, making it easier for users to specify what they want, communicating back about the tool needs, and improving the overall flow so the tools can be used much more effectively by a broader range of customers and knowledge levels.

Zhang: If I look at the past 20 years, what are some of the major changes along the way that have really promoted formal to the broader user base? The standardization of SystemVerilog assertions was a key part of it, and the proliferation of formal as a technology in different domains. The app-specific solutions created around tools helped in finding all the different use cases where formal can be used, maybe without expertise. That was a great venture, which broadened formal application. Another one that comes to mind is formal sign-off. Before then, formal was always seen as a debugging tool. If you can’t sign off on a block, it becomes a nice-to-have, maybe not a must-have. But once you can do sign-off, and bounded sign-off, when you have a methodology that really helps people see formal in a more serious light, you can really deploy it in the flow. Lately, with the machine learning infusion, and more recently GenAI, a lot of things that are happening are major milestones that promoted formal to being regarded as part of the verification flow. There’s a lot less missionary selling that we have to do these days. All the other things behind the scenes, that the R&D teams are working on — standardization, the methodology — contribute to formal. It’s really a mainstream tool every company is using these days.

SE: We hear a lot about advancements in data centers, new technologies like CXL and HBM. Formal has always been limited by the amount of memory that it needs and the amount of compute that it needs. Theoretically, now we have infinite memory and infinite compute. How much is that helping formal?

Levitt: These new architectures reliably give you a linear speed-up, but the problems are exponential, or at least NP hard. We’ll take that, but I would still say most of the advances are being driven by improvements in the SAT solvers. Those are getting exponentially better. Improvements in engineering related to the algorithms we run, and how we orchestrate them, also are getting exponentially better. Increased compute power, we’ll take that, but it is a linear speed-up, sometimes super-linear if it enables you to do more things at once. But the real performance improvements are still coming at the fundamental SAT solver level, and at the algorithm level, not from the increased availability of resources.

Darbari: Apart from the SAT solver efficiency, how you model things makes a significant difference with abstraction. I have a very good example from recent work, which we presented at DVCon India, of a RISC-V processor. It had a five- to six-stage deep pipeline running on a machine with 1.5 terabytes of RAM with 96 cores. We got a bounded proof at 10,331 cranks. Trying to prove that one instance of an ‘add’ instruction can be sent in the pipe and can actually execute correctly. Never mind the entire space of instructions, just one ‘add’ instruction. We then went through the process of breaking it down and bringing in coverage analysis and abstraction engines. We were then able to prove that same property in about 100 seconds with the bound of 18. The only reason we couldn’t prove it earlier was because there was a live lock in the processor. We went about finding it, and because it’s an NP hard problem, and in one go, we are trying to verify all instances of operands and all the cases. If any one of these cases encounters a hump, the proof is stuck. You can throw the biggest machine at it, but you can’t actually make a difference. People who have been using formal understand that. Would I be able to get the same result on a smaller machine? In this case, when we did throw the same testbench on an 18-core machine with 128 gigabytes of RAM, we also got the proofs, except it took a little bit longer. Compute will make a difference, but it’s asymptotic, and throwing more compute at the problem wouldn’t make a significant difference unless we understand what is being verified and how it is being modeled.

Safarpour: If we look at it from the user’s problem perspective, Ashish is talking about a problem with a single property that’s hard to prove, and there are always these cases. But what we’re seeing is that the vast size of the problem, and the sheer number of properties that they’re trying to work on, is orders of magnitude bigger than previous generations. It’s not uncommon to hear from our customers that in a formal property verification setup, not connectivity or coverage or anything like that, they have hundreds of thousands, if not millions, of properties that they need to prove. In these setups, compute makes a really big difference. If you have hundreds of cores available or thousands of cores available, big memory machines, there’s a lot that you can do. While proving one property can always be hard, one of the challenges that we find ourselves having to solve is one of management. You have hundreds of thousands of properties, you have hundreds of cores at your disposal. Even when you’re running this nightly for regressions, or over a week, there are properties that have not gotten enough time for any single engine to work on it. You have to innovate, because in the past you wouldn’t have problems that are as broad as they are now. The sheer volume of what our customers bring to us has become a major challenge. The machine availability is there, but what we need to do on the orchestration side and smart deployment really plays a critical role. Customers do come to us and ask, ‘What if I give you 10,000 cores? What if I give you 100,000 cores for a few hours? Could you crack this?’ It is opening up this massively parallel domain. This is great. The problems are getting harder. The compute is available. That allows us to tackle these new sets of problems.

Zhang: From a tool perspective, we definitely want to leverage parallelization, leverage all the compute. But the reality is that customers don’t have unlimited compute. We are still working with the constraint that there’s only so much compute we can give you, and we’re competing with simulation and all the other tools. There’s the real-life limitation, but on the technology side, there are a lot of advancements that are taking advantage of what we can do to parallelize jobs, orchestrate it in a way that’s most efficient, leveraging previous results. All of those improvements are from the tool perspective. But I wish we had unlimited compute.