Towards the verification of communications in NoC architectures



This work addresses the validation of the communication infrastructure in NoC (Networks on Chip) centered designs.
A theorem proving based solution enables the verification of high-level properties for NoC communication algorithms, and a complementary approach (oriented toward Assertion-Based Verification) focuses on the verification of RT level implementations. It is also applicable to the on-line checking of robustness properties.

1. A formal theory of communications in NoCs

Our method for formally verifying high-level properties for NoC communication algorithms is based on a generic formal model for the representation of the communications on a chip, called GeNoC. This model is implemented in the ACL2 theorem prover.

The model

The model gives an abstract view of the Transport (4), Network (3) and Data Link (2) layers of the OSI model. It is parameterized by various characteristics of the NoC: its topology and size, routing and switching techniques.

Its definition assumes that each node is made of an application and an interface, and mainly relies on the following functions: These functions are not given explicit definitions. Rather, they are characterized by the set of properties they should satisfy, called proof obligations or constraints.

Proof of correctness

It has been proven, once and for all in the meta-model, that this set of proof obligations implies two correctness theorems, which state that: Proving that a particular NoC is a valid instance of GeNoC, and thus satisfies those correctness theorems, amounts to:

Results

This model has been used to perform formal verification on various communication infrastructures, such as We distribute here a stable version of GeNoC (August 2008), with the proof of the Spidergon.

Moreover, ACL2 provides both a theorem prover and an execution engine in the same environment, since its specification language is the programming language Common Lisp. Theorems can be proven for the functions we define in ACL2, and the same function definitions can also be executed. Thus we can get confidence in our formal model by comparing ACL2 executions with, for instance, VHDL simulations.
Here are examples of ACL2 simulations of Hermes and Spidergon, animated through a Java graphical interface:

          

An example of ACL2 simulation of Nostrum (animated through the Java graphical interface) can be found here.

2. General purpose properties for Assertion-Based Verification

GeNoC targets the verification of high-level (algorithmic) properties about the complete network. Hence the NoC description is made at a high level of abstraction, ignoring several implementation details. The complementary Assertion-Based Verification (ABV) oriented solution targets the verification of properties for RT level implementations, thus enabling the verification of the correct functionality of the NoC from the design phase up to the run-time phase.

Classification of typical properties

We have proposed a comprehensive and abstract definition of properties that NoC implementations should satisfy, and examples of their PSL formalization for Nostrum and Hermes (NoCs'2012). These properties take into account various NoC features (buffered communications or not, synchronous or not, switching techniques, deterministic routing or not,...), and address: Example: here is a property in the category "no packet loss" instantiated for Hermes and Nostrum

Results

For Nostrum and Hermes, the PSL assertions have been transformed into synthesizable Horus monitors and the VHDL descriptions have been instrumented with these checkers: a total of 39 PSL assertions have been created for Nostrum, and 30 for Hermes.

Here is an example of instrumented Hermes simulation with fault injection: a violation is caused for assertions "an acknowledgment is sent only if the router receives a request and the corresponding packet/flit" and "if the sender receives an acknowledgment it will stop requesting for transmission" of category "no packet duplication". We can see that the "valid" outputs of the corresponding assertion checkers (monitors) indicate the violations.


The assertions have also been synthesized with their NoC into a Virtex 5 Xilinx FPGA. For instance, a 4x4 version of Hermes has been synthesized with 7 monitors connected to each of six central routers (and with traffic generators). The area and speed with the monitors are 22581 LUT and 48.25 MHz (21173 LUT and 64 MHz without monitors).


References

Contact

Laurence PIERRE
TIMA Laboratory
Laurence.Pierre@univ-grenoble-alpes.fr
Tel. +33 (0)4 76 57 49 92