Blog

Ashish Darbari, founder and CEO of Axiomise, speaks to Microelectronics UK on making formal normal, why designs are getting harder and schedules shorter, and his three big bets for the future. Many thanks to Ashish for providing these answers.

---

Tell us about your role and what Axiomise does - what problems are you solving, and for whom? 

I'm the founder and CEO of Axiomise, a company I started in 2017 to make formal normal, turning it from a specialist technique into a mainstream route to deterministic sign-off. We provide training, consulting, services and vendor-neutral formal verification apps to help semiconductor teams find deep corner-case bugs and mathematically prove their absence in complex designs, from RISC-V and Arm processors to GPUs, networking blocks and AI/ML hardware. Over the last 8+ years we've worked with more than 22 customers from AMD and Akeana to Bluespec and CDAC, trained over 1600 engineers, most recently helping Akeana formally verify its super-scalar RISC-V core ahead of tape-out.

What are the defining technical and operational pressures facing your sector right now - and where do you see the industry underestimating the challenge?

The defining pressure is that designs are getting exponentially harder while schedules are getting shorter. Modern SoCs combine super-scalar out-of-order RISC-V and Arm cores, GPUs, NoCs, mixed-precision AI accelerators moving between FP8 and FP4, and increasingly CHERI-style security extensions, and every one of these is a corner-case minefield that constrained-random simulation and FPGA prototyping cannot exhaustively cover. On top of that, teams are being asked to tape out at advanced nodes where a respin easily costs tens of millions of dollars, and geopolitical and supply-chain pressure means there is no margin for a functional escape or a late PPA surprise.

Operationally, the sector is short of experienced verification engineers, and the ones it has are being pulled between simulation, emulation, formal, and now AI-assisted RTL flows, without a clear methodology tying them together. AI copilots are accelerating RTL productivity, which is welcome, but they also generate more code, more variants and more opportunities for silent bugs to slip through, so the verification debt per engineer is rising, not falling.

Where the industry consistently underestimates the challenge is in assuming that more simulation cycles, more emulation hours, or a smarter AI copilot will close the gap. They will not. Coverage-driven simulation can only sample the state space, and no amount of AI-generated stimulus turns sampling into proof. The bugs that actually kill tape-outs, deadlocks and livelocks in out-of-order pipelines, arithmetic edge cases in mixed-precision datapaths, ordering violations in NoCs, silent power-burning redundant logic, security holes at the HW/SW boundary, are exactly the ones only exhaustive formal proof can find and, just as importantly, prove absent. The industry treats formal as an optional add-on when it should be the sign-off backbone, and that gap is what we built Axiomise to close.

Which application areas or end markets present the strongest near-term opportunity for your technology, and what is driving that demand? 

The strongest near-term pull is AI/ML silicon and RISC-V, which is where the combination of aggressive schedules, mixed-precision arithmetic and huge parallel datapaths breaks traditional verification. Hyperscalers and AI startups are taping out custom accelerators with FP8 and FP4 datapaths, systolic arrays, and on-chip networks that move tensors between hundreds of compute tiles, and they simply cannot afford a functional or PPA escape at 4nm and below. Our floatrix app for end-to-end floating-point proofs, nocProve for on-chip network correctness, and footprint for catching silent power-burning redundant logic map directly onto that problem, and the demand is being driven by the economics of a single respin as much as by the correctness risk.

RISC-V is the second major pull, and it is accelerating faster than most people expected. Super-scalar out-of-order RISC-V cores are moving into performance sockets that used to be Arm-only, from client compute to automotive and datacentre, and every one of those designs needs ISA-level and micro-architectural sign-off that constrained-random simulation cannot deliver. Our formalISA app, powered by CoreProve, gives teams vendor-neutral exhaustive proofs against the RISC-V ISA, which is why we have been engaged on production cores at Akeana, Bluespec and others, and why the RISC-V community keeps coming back to formal as the only credible path to sign-off.

The third area, and the one I expect to grow fastest over the next 24 months, is high-assurance and security-critical silicon: automotive, aerospace, defence, and the emerging CHERI-based secure compute stack. Regulators and OEMs are moving from "tested" to "proven" as the bar, safety standards such as ISO 26262 and DO-254 reward mathematical evidence, and CHERI in particular needs formal proof at the HW/SW interface because the whole point is capability enforcement that cannot be bypassed and it needs to be demonstrated through a proof. Underneath all three markets sits the same driver: silicon is now too expensive, too complex and too consequential to sign off on samples of the state space, and customers are recognising that exhaustive proof is the only sign-off currency that scales.

Which emerging technologies or engineering approaches are you backing for the next three to five years - and what would it take for them to cross from promising to mainstream?

The first bet is exhaustive, proof-convergent formal verification as the default sign-off backbone, not a specialist add-on. Our own investment here is CoreProve, our proof-convergence engine, and the Axiomiser platform that wraps formalISA, floatrix, nocProve and footprint into a single vendor-neutral flow. For this to cross from promising to mainstream, three things need to happen: EDA vendors need to keep opening up their engines to methodology-driven flows, universities need to teach formal alongside simulation from day one, and design leaders need to accept that "proven" is a cheaper long-term currency than "tested a lot".

The second bet is AI-assisted design and verification, but with a very clear split of responsibilities. I back AI copilots for RTL productivity, PPA exploration, SVA drafting and debug triage, and we are already using specialised local models internally for exactly those tasks. What I do not back is the idea that a large language model will ever replace exhaustive proof. Formal gives you a mathematical guarantee; AI gives you a plausible suggestion, and the two are complementary, not interchangeable. For AI to cross into mainstream verification use, the industry needs auditable, private-by-default deployments so confidential RTL never leaves the customer boundary, and it needs benchmarks that measure correctness impact, not just token throughput.

The third bet is compositional and abstraction-led verification for the designs that are now too big to attack monolithically: super-scalar out-of-order cores, systolic AI accelerators, chiplet-based SoCs, NoCs at scale, and finite-field arithmetic blocks such as BCH and elliptic-curve ECC. We are actively extending our proof harnesses in this direction, combining arithmetic proofs, transport proofs, scheduling assertions and inductive accumulator theorems into end-to-end sign-off. The blocker to mainstream is skills and methodology, not tool horsepower. When enough verification leads know how to decompose a proof, compositional formal will feel as routine as UVM does today, and that is exactly the gap our training programme is designed to close.

Events like Microelectronics UK bring together engineers, researchers, and industry decision-makers under one roof. How valuable is that kind of in-person concentration of expertise to you and your team?

Extremely valuable, and this year even more so, because I'm moderating the panel on AI and IoT in embedded cybersecurity with panellists from JLR, Eurostar and the University of York. Having engineers and researchers from organisations of that calibre in one room shifts the conversation from theory to the real trade-offs teams are wrestling with: how to secure IoT systems by design, where machine learning genuinely helps with threat detection, and which embedded vulnerabilities the industry is quietly underestimating. That density of expertise, compressed into a single session, is almost impossible to replicate any other way, and the corridor conversations that follow are where real collaborations start.

What do you want engineers and technical buyers to come away understanding about Axiomise after speaking with you at the show - and what conversations are you expecting to have on the floor?

The one thing I want engineers and technical buyers to walk away understanding is that Axiomise is not another EDA vendor selling engines, we are the vendor-neutral formal verification partner that turns those engines into deterministic sign-off. That means exhaustive proofs of correctness, not sampled coverage, on the hardest blocks in modern silicon: super-scalar RISC-V and Arm cores, GPUs, NoCs, mixed-precision AI accelerators, and the HW/SW boundaries that increasingly carry security guarantees. Our combination of the Axiomiser platform, CoreProve, and apps like formalISA, floatrix, nocProve and footprint, together with our training and services, is what has let customers such as AMD, Akeana and Bluespec ship confidently at advanced nodes.

The conversations I'm expecting, both on the floor and around the panel, fall into three buckets. The first is engineers asking very concrete questions: how do you close proofs on an out-of-order pipeline, how do you verify a systolic array end-to-end, and how do you catch redundant power-burning logic that simulation never flags. The second is verification and design leads who know formal is the answer for their next tape-out but are wrestling with methodology, skills and how to justify the investment internally, which is where our training and consulting practice comes in. The third, sharpened by the AI and IoT cybersecurity panel I'm moderating, is technical buyers and executives asking the harder commercial question: what does exhaustive sign-off actually cost, and what does a functional escape, a late PPA surprise or a security breach cost if we do not do it.

If people leave the event with one sentence in their heads, I want it to be this: formal verification is no longer optional for high-assurance silicon, and Axiomise is how you make it normal.

Is there a leader, engineer, or mentor who has shaped how you approach your work - and what is the most enduring lesson you took from them? 

My role models are the researchers whose work I grew up studying, and whose ideas quietly shaped every stage of my education, from my early engineering degree in India, to my masters in Germany, to my doctorate at Oxford in formal verification. The lineage runs from Steffen Hoeldobbler, Paola Bruscoli and Alessio Guglielmi at Dresden. These people shaped my initial journey in formal methods. Tom Melham at Oxford gave me an opportunity to work on my doctorate with a great internship opportunity with Intel and introduced me to Mike Gordon at Cambridge. Together, Mike and Tom have inspired me to pursue excellence no matter what. Sir. Bashir Al Hashimi now at Kings College who gave me my first Postdoc opportunity on fault simulation with formal. Joao Marques Silva inspired me to design a formally correct certified SAT solver. Many more in industry and research partnerships - John O’Leary at Intel, John Penton and Ashan Pathirane at Arm,  S. Ramesh at GM, Supratik Chakaraborty at IIT Bombay, Theo Drane at AMD, Ziyad Hanna at Cadence, Manish Pandey at Synopsys, Harry Foster and Dennis Brophy at Siemens. The underlying message is professional integrity and pursuit of excellence.

What does the next 12 months look like for Axiomise - in terms of product direction, capability expansion, or where you are focusing development resource? 

The next twelve months are about scaling Axiomise into a domain-specific sign-off platform, tuned to the verification realities of the markets where the cost of a functional escape is highest. On the product side, our development resource is focused on three fronts. First, deepening CoreProve, our proof-convergence engine, so that increasingly large and out-of-order designs can be closed exhaustively rather than sampled. Second, extending the app portfolio: floatrix into the mathematics behind error-correcting codes such as BCH in flash memory and elliptic-curve cryptography in secure boot and post-quantum designs, so these blocks get the same exhaustive rigour we already apply to floating point, nocProve into larger and more heterogeneous on-chip and chiplet networks, and footprint into deeper PPA and silent power-burner detection. Operationally, we are investing hard in two adoption channels. Our training programme, which has already upskilled over 1,600 engineers, is being expanded with more instructor-led cohorts and a refreshed e-learning portal, because the biggest single blocker to mainstream formal is skills, not tools. And we are broadening our commercial reach into North America and the EU, including through the EuroCDP route for the European semiconductor ecosystem, so fabless startups and design houses can access Axiomise expertise closer to home.

The strategic thread underneath all of it is the same message we take into every customer conversation and every event, including Microelectronics UK: silicon is now too expensive and too consequential to sign off on samples of the state space, and our job over the next years is to make exhaustive, deterministic sign-off the normal way to tape out, not the exceptional one.