​NoC verification: why simulation is not enough

Modern AI and high‑performance SoCs depend on network‑on‑chip (NoC) fabrics to move data between hundreds of processing elements and memory. A coherent NoC based on protocols like Arm CHI or ACE sits at the heart of every cache line, snoop, DMA transfer and interrupt. That fabric must guarantee not just correct data transport, but correct cache coherence across the entire system.

Traditional simulation, even with sophisticated UVM testbenches or fuzzing, cannot realistically explore all interleavings of transactions, virtual channels, credits, routing‑table changes and power/clock‑domain crossings. The most dangerous corner‑case bugs live in tiny regions of the state space that no practical simulation budget will reach.

Hidden bug families in coherent NoCs

Real NoCs exhibit recurring high‑impact bug families, including:

• Flow‑control and credit accounting errors that silently overwrite in‑flight data.

• Ordering and serialization violations that produce impossible memory states.

• Coherence state‑machine bugs where caches and home nodes silently disagree on line state.

• Deadlocks and livelocks caused by stranded flits, unfair arbitration or NodeID aliasing.

• Reset, power and clock‑domain crossing hazards, X‑propagation and control‑field corruption in transit.

• Security and side‑channel leaks across Secure/Non‑Secure or multi‑tenant domains.

These bugs often appear structurally clean, all flits are well‑formed, parity/ECC pass, RAS sees no error, yet the system data is corrupted or frozen.

Why formal verification changes the game

Formal verification for NoC designs uses mathematics to exhaustively prove that key properties hold across all reachable states  or to provide counterexample traces when they do not. For NoC verification, that means:

• Proving end‑to‑end invariants (ordering, coherence, forward progress) across the entire fabric.

• Exploring deep combinations of preconditions that rarely occur in tests but do arise under real workloads.

• Turning “we didn’t see a bug in billions of cycles” into “we have a proof of bug absence or a concrete failing trace.”

Axiomise’s nocProve app, built on the CoreProve proof technology, is designed specifically for exhaustive formal verification of NoCs: it scales across AXI, ACE, ACE‑Lite and CHI; across mesh, ring and crossbar topologies; across multiple virtual channels and transaction classes. It automates invariants and abstractions so design teams can verify complex NoCs with practical run times instead of handwritten formal testbenches.

Example: deadlocks and silent data corruption

The full article shows real NoC bugs that evade simulation, such as:

• Silent data corruption in an AXI reorder buffer where responses with the same ID overwrite each other.

• Deadlock caused by non‑atomic NodeID rebinding in a CHI mesh, where routing‑table updates and in‑flight responses interact to stall progress without any protocol error.

These examples illustrate why NoC verification with formal methods is now essential for AI, HPC, automotive and data‑center silicon.

Read the full article on Semiconductor Engineering

If you’d like to dive deeper into the bug families, real‑world examples and how nocProve scales to full mesh configurations, you can read the full blog post on SemiEngineering. 

👉 Why Your NoC Verification Strategy Must Consider Using Formal