Sign-off every NoC using nocProve with 100% proof convergence
LONDON, UK / ACCESS Newswire / March 2, 2026 / Axiomise announced the launch of a new app called nocProveTM that automates the verification of custom implementations of network-on-chips (NoC) with exhaustive guarantees generated by formal proofs.
Modern-day HPC and AI chips are powered by sophisticated NoCs needed to handle high-bandwidth and low-latency traffic. Every prompt you make on an LLM, routes packets on a NoC. With the advent of custom AI architectures, the industry is seeing a massive influx of custom NoC implementations, and they are notoriously difficult to verify due to their size and challenges of deadlocks and livelocks. Complexity of a NoC is often increased by several folds due to micro-architectural optimizations using virtual channels, multi-clock domains, clock-gating, and programmable interfaces with a range of protocols such as AXI4, AXI5, ACE, CHI etc. Ensuring that the traffic is never blocked in the NoC is critical to ensure functional correctness. At the same time, performance is a critical barrier in NoC implementations. nocProve addresses these complex design verification challenges.
nocProve is a custom configurable app within the axiomiser® platform designed by Axiomise to tackle some of the largest NoCs the semiconductor industry is building. Most seasoned engineers in the industry know that getting full (exhaustive) proofs is very hard for most designs including NoCs as it involves a great deal of non-determinism. The nocProve app is powered by the abstraction proof engine technology called CoreProve® that tackles the challenges of bounded (undetermined) proofs. For years, the Axiomise R&D team has been developing proof engineering techniques to handle proof convergence across the board for all kinds of design verification using formal. Axiomise is proud to bring the nocProve app to the market driven by CoreProve.
The app can be configured to handle different bus protocols, different channel types, as well as complex routing rules to ensure that an implementation developed in Verilog or VHDL conforms to the specification rules specified in SystemVerilog Assertions (SVA) through a full formal proof. The nocProve app automates critical functional and performance verification tasks for exhaustive proofs within a few hours of run time finding critical bugs. The best outcome obtained from nocProve is a combination of corner-case bug hunting, and full proofs allowing for a significant reduction in time-to-market.
“Finding the last bug is equally important to finding the very first one, as software fixes on post-silicon bugs would cause a dramatic reduction in performance in the best case, or an entire respin in the worst case. We are super excited to announce the launch of nocProve. This app allows us to prove complex implementations of NoCs with ease – without needing a huge team of engineers to manually architect testbenches which may or may not yield proof convergence. Once the app is configured, it allows designers to get visibility into bugs right on the very first day, without having any verification code to be written”, says Dr. Ashish Darbari, CEO, Axiomise Limited.
The nocProve app is ready for deployment on commercial-grade NoCs and has been shown recently to verify the open-source FlooNoC design from the PULP platform. FlooNoC is a PULP platform NoC with 645 Gb/s per link and an aggregate ~103 Tb/s for an 8×4 mesh with 288 RISC‑V cores, at ~3.5% area overhead per tile and ~0.15 pJ/B/hop energy. It fully supports AXI4 and ATOPs protocols with bursts and multiple outstanding transactions providing end-to-end ordering and ID tracking.
“The app is very easy to configure and use. As an example, one of our graduate engineers used it to verify the FlooNoC design exhaustively under 4 hours”, adds Dr. Darbari.
About Axiomise
Axiomise accelerates formal verification adoption through its unique combination of consulting, services, training, and custom software solutions. Axiomise is headquartered in the UK and was founded by Dr. Ashish Darbari (FBCS, FIETE, DPhil Oxon) and Dr. Vidya Chandran Darbari (PhD Cantab, MBBS, MRSB, FHEA). In the last 8 years, Axiomise has helped over 20 customers with a unique combination of formal verification training, having trained over thousand engineers and helping some of the biggest names in silicon design with its consulting & services and custom apps.
Engage with Axiomise at:
Website: http://www.axiomise.com
Twitter: @axiomise
LinkedIn: https://www.linkedin.com/company/axiomise/
Facebook: https://www.facebook.com/axiomise
Axiomise, axiomiser, CoreProve, footprint, formalISA, floatrix and the Axiomise logo are trademarks of Axiomise Limited, UK.
For more information, contact:
Fabiana Muto
Public Relations for Axiomise
+44 1442 345 046
[email protected]
SOURCE: Axiomise Ltd.
