Akeana Partners with Axiomise for Formal Verification of Its Super-Scalar RISC-V Cores

Akeana Inc. announced a key milestone in the development of its advanced RISC-V technology: a successful partnership with Axiomise Limited to formally verify its super-scalar test chip, Alpine. The collaboration highlights the growing importance of formal verification in ensuring correctness, performance, and efficiency in next-generation semiconductor designs.

Alpine is a 4nm silicon and software development board that integrates high-performance, out-of-order RISC-V cores. As semiconductor process nodes continue to shrink and architectural complexity increases, ensuring functional correctness before tape-out has become both more challenging and more critical. Super-scalar, out-of-order cores, designed to execute multiple instructions per clock cycle, introduce intricate control logic, speculative execution paths, and numerous corner cases that are difficult to fully validate using traditional simulation techniques alone.

To address these challenges, Akeana turned to Axiomise for its deep expertise in formal verification. Unlike simulation-based approaches, which rely on test vectors and probabilistic coverage, formal verification applies mathematical proof techniques to exhaustively analyze all reachable states of a design. This guarantees that specific properties hold true under every possible condition, eliminating entire classes of latent bugs that could otherwise escape detection.

According to Nitin Rajmohan, Co-founder of Akeana, the results of the engagement exceeded expectations. Within just a few months, Axiomise’s team not only identified functional issues but also uncovered potential redundant logic in the design—findings that were not anticipated at the outset. These insights provided Akeana with opportunities to further optimize its RTL before tape-out, reducing risk and improving overall design quality. The experience reinforced the long-term value of formal verification within Akeana’s broader development methodology.

Axiomise employs a structured methodology that combines expert consulting with proprietary applications such as formalISA®, footprint®, and floatrix®, powered by its CoreProve® framework. These tools are designed to achieve full proof convergence using commercial EDA platforms, enabling end-to-end formal verification sign-off. By integrating advanced automation with domain-specific expertise, Axiomise delivers mathematically rigorous results across functional correctness, performance constraints, and area optimization.

For a complex 4nm design like Alpine, this approach provides significant advantages. At advanced process nodes, the cost of a silicon re-spin can be enormous, not only financially but also in terms of market timing and competitive positioning. Formal verification reduces this risk by ensuring that corner cases, particularly those involving concurrency, memory ordering, branch prediction, and pipeline hazards, are thoroughly analyzed before fabrication.

Beyond functional correctness, the partnership also addressed PPA (Power, Performance, Area) considerations. While verification is traditionally associated with functional validation, formal methods can also reveal inefficiencies in control logic or data paths that affect power consumption and silicon footprint. By identifying redundant or suboptimal structures early, Akeana was able to make informed design refinements that support both performance targets and area constraints.

Dr. Ashish Darbari, CEO of Axiomise, emphasized the broader industry significance of the project. As RISC-V adoption accelerates across markets—including mobile, automotive, data centers, and cloud computing—the demand for high-performance, reliable cores continues to grow. Formal verification provides the exhaustive guarantees required for these mission-critical applications, where undetected design flaws can have far-reaching consequences.

The tape-out of Alpine represents a meaningful milestone not only for Akeana but also for the expanding RISC-V ecosystem. It demonstrates that open-standard architectures can meet the stringent quality and performance expectations traditionally associated with proprietary designs. By incorporating formal verification at a sign-off level, Akeana underscores its commitment to delivering robust, production-ready IP to its customers.

Headquartered in Santa Clara, California, Akeana is backed by prominent investors including Kleiner Perkins, Mayfield Fund, and Fidelity Ventures. The company focuses on configurable RISC-V-based compute, interconnect, and AI accelerator IP solutions. Axiomise, based in the UK, has built a reputation over the past eight years for advancing formal verification adoption through consulting, training, and custom software solutions.

Bottom line: The two companies have demonstrated how collaboration between IP innovators and formal verification specialists can accelerate development while maintaining uncompromising quality standards. As semiconductor designs grow increasingly complex, partnerships like this are likely to become essential in ensuring that next-generation silicon achieves both performance leadership and mathematical correctness from day one.

CONTACT AKEANA

CONTACT AXIOMISE