A high-quality verification campaign including methods able to absolutely prove the correctness of critical design behaviors as a complement to mainstream dynamic verification? At first glance this should be a no-brainer. Formal verification offers that option and formal adoption has been growing steadily, now used in around 30-35% of designs per the Siemens/Wilson Research Group survey. However anecdotal evidence from formal verification service companies such as Axiomise suggests that real benefit extracted from formal methods still falls significantly short of the potential these methods can offer. A discussion with Dr Ashish Darbari, CEO of Axiomise, prompted this analysis of that gap and how it can be closed.
What’s going on?
About half of reported usage is attributable to support apps which make canned checks more accessible to non-expert users. The balance comes in straight property checking, a direct application of formal engines for which you must define all required assertions, constraints, and other factors in constructing proofs. Apps offer a bounded set of checks; property checking offers unbounded options to test whatever behavior you want to prove.
The complexity of formulating an efficient property check is another matter. Like any other problem in CS, problem complexity can span from relatively simple to difficult to practically insoluble. By way of example, consider a check for deadlocks. In a single finite state machine (FSM) such a check is sufficiently easy to characterize that it is included in standard apps. Checking for possible deadlocks in multiple interacting FSMs is more challenging to package because problem characterization is more complex and domain specific. Checking for deadlocks in a network on chip (NoC) is more challenging still given the span, topology, and size of a typical NoC. Cross-sub-system proofs or proofs of behavior under software constraints I suspect are beyond the bound of methods known today (without massive manual abstraction – I’d be happy to hear I’m wrong).
Another complication is that while many argue you don’t need to be a mathematician to use these methods, effective formal attacks to complex problems still very much depend on finesse rather than brute force. You may not need a math degree but you do need something of a mathematical or at least a puzzle mindset, constantly reinforced. I think this is why successful formal verification deployments run as separate teams. Dynamic verification teams also face difficult challenges but of a different kind. It is difficult to see how one person could routinely switch between both domains and still excel in each.
In this light, outsourcing for complex formal verification objectives becomes inevitable, to specialists with concentrated and growing experience in that domain. Axiomise certainly seems to be benefiting from that demand, not just from small ventures but from major names among semiconductor and systems enterprises.
Why Axiomise?
Axiomise provide consulting and services, training, and an app they call formalISA for RISC-V formal verification. Apps of this type may ultimately add a high margin revenue component to growth though it appears today that clients prefer a full turnkey solution, for which formalISA underlies a value-added service.
Ashish and his CTO Neil Dunlop have extensive experience in formal methods. The rest of the technical team are mathematicians, physicists, and VLSI experts trained from scratch in Ashish’s approach to formal problem solving. This they have applied across a wide variety of subsystems and test objectives. One very topical application is for RISC-V cores.
Extensibility and multiple sources for cores are key strengths for RISC-V but also come with a weakness I have mentioned before. Arm spends between $100M and $150M per year in verification; Intel and AMD probably spend much more. They have all built up decades of legacy verification assets, spanning many possible CPU variants and optimizations. To rise to comparable verification quality on an unmodified RISC-V core is a major task, given a staggering range of test scenarios which must be covered against a wide range of possible architecture optimizations. Add in a custom instruction or two and the verification task is amplified even further.
Formal methods are the ideal way to prove correctness in such cases, assuming an appropriate level of finesse in proofs. Axiomise use their formalISA app to run push-button proofs on correctness on 32-bit and 64-bit implementations, and they have production-ready implementations for RV32IMC and RV64IMC instruction sets. Examples of problems found include a bug in RISC-V specification v 2.2 and over 70 deadlocks found in the previously verified zeroriscy. The app found new bugs in the ibex core and architectural issues with LOAD instruction in zeroriscy. It found 30 bugs in WARP-V (2-stage, 4-stage, and 6-stage in-order cores) and cv32e40p core from OpenHW. Axiomise has also verified the out-of-order execution CVA6 core using formalISA. Details of these bugs are available on GitHub.
As usual, the development involved in these tests is a one-time effort. Once in place, regressions can be run hands-free. Ashish tells me that with formalISA, diagnosis of any detected problem is also simplified.
Takeaway
I’d like to believe that in time, more of these kinds of tests can be “app-ified”, extending the range of testing that can be performed in-house without service support. Today building such tests require a special level of formal expertise often only available in long-established centers of excellence and in organizations such as Axiomise. Since other big semiconductor and systems companies are happy to let Axiomise consult and train their teams to better corral these complex problems, you might want to check them out when you face hard proof problems.
You can learn more about Axiomise HERE, the formalISA studio HERE and the RISC-V studio HERE.
Also Read:
2024 Outlook with Laura Long of Axiomise
RISC-V Summit Buzz – Axiomise Accelerates RISC-V Designs with Next Generation formalISA®
WEBINAR: The Power of Formal Verification: From flops to billion-gate designs
Share this post via:
TSMC Unveils the World’s Most Advanced Logic Technology at IEDM