Axiomise Introduces nocProve to Transform NoC Design Verification

Axiomise has recently launched a new verification tool called nocProve which will transform how Network-on-Chip designs are validated in modern hardware development, absolutely.

The tool is designed to be the first configurable formal verification application specifically created for NoC implementations. It addresses one of the most complex challenges faced by semiconductor engineers and promises to provide a more efficient and thorough approach to ensuring correctness in advanced chip designs.

A Network-on-Chip serves as the communication backbone of complex integrated circuits. These networks route information between processor cores, memory controllers, and specialized accelerators within a chip. NoCs are critical to achieving high bandwidth, low latency, and reliable operation. Every instruction or data transfer in high-performance computing tasks or artificial intelligence workloads relies on these networks functioning correctly. As new custom AI architectures and multi-core processors emerge, designers are creating bespoke NoC configurations to maximize performance and support novel protocols. These custom designs, however, introduce significant verification challenges due to their complexity, multiple clock domains, virtual channels, and advanced routing schemes. Errors such as deadlocks or livelocks can occur in rare circumstances that traditional simulation techniques may not detect.

Formal verification is a method that mathematically proves a design meets its specification under all possible conditions. It is considered the gold standard for ensuring reliability in critical systems. Despite its advantages, formal verification has historically been difficult for NoCs due to the large number of possible states and the nondeterministic behavior of complex designs. Axiomise built nocProve as a configurable application within its existing platform using the company’s proprietary proof engine. This engine is optimized to handle the challenges of formal verification for large, nondeterministic systems. It allows engineers to prove the correctness of their designs exhaustively while reducing the computational burden that often prevents formal methods from completing successfully.

The tool can be adapted to a wide variety of bus protocols, channel types, and routing policies. Engineers submit their designs, usually in hardware description languages such as Verilog or VHDL, along with assertion specifications written in SystemVerilog Assertions. nocProve automatically generates formal proofs to verify that the design conforms to the specifications. This approach allows engineers to catch subtle bugs and corner-case errors that could otherwise go unnoticed until after production. By automating these tasks, nocProve also saves time and reduces the need for labor-intensive manual verification efforts.

The launch of nocProve is significant because traditional verification techniques such as simulation or constrained random testing can only examine a finite set of scenarios. These methods may miss rare but critical faults that could cause functional errors or degrade performance. Formal verification using nocProve provides exhaustive confidence that the design is correct, which is particularly important for high-stakes applications in artificial intelligence accelerators, data centers, and high-performance computing chips. Early detection of potential faults reduces the risk of expensive post-production fixes and silicon respins that can delay product launches.

Axiomise has demonstrated nocProve on real-world NoC designs. The tool was able to verify complex open-source designs with high throughput and multiple simultaneous transactions within a few hours. This speed and reliability showcase the potential for nocProve to be integrated into modern chip development workflows and provide meaningful results early in the verification process. The automation of formal proofs allows design teams to innovate more quickly and with greater confidence, ensuring correctness without sacrificing development time.

Bottom line: nocProve represents a major advance in the formal verification of Network-on-Chip architectures. By automating exhaustive proof generation and efficiently handling complex designs, it addresses one of the semiconductor industry’s most pressing verification challenges. As chips become more customized and performance demands continue to grow, tools like nocProve will be essential for ensuring reliability while accelerating development and reducing the risk of costly errors. Axiomise’s new tool promises to give engineers the confidence to build advanced systems without compromising on correctness or speed.

CONTACT AXIOMISE

Also Read:

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

IP Surgery and the Redundant Logic Problem

Podcast EP274: How Axiomise Makes Formal Predictable and Normal with Dr. Ashish Darbari