Presentation of GeNoC

Towards a formal theory of communications in NoC architectures

This work addresses the validation of the communication infrastructure in NoC (Networks on Chip) centered designs.

Our method for formally verifying the correctness of the communication operations 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:

at the Transport layer, interfaces are represented by two functions used to encode messages to be sent in the network (send) and to decode them (recv). Function R4D ("ready for departure") determines which messages can be in the network at the current time. Messages may be injected only at a specific execution time, or under constraints on the network load (e.g., credit-based flow control),
at the Network layer, the routing algorithm is represented by function Routing and the switching technique is represented by function Scheduling. The routing algorithm is represented by the successive application of unitary moves (e.g., routing hops). The model also allows the modeling of priorities between messages (e.g., using a Round Robin policy),
at the Data Link layer, the transmission protocol is specified.

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:

every message arrived at some node n was actually issued at some source node s and originally addressed to node n, and it reaches its destination without modification of its content,
no message is lost.

Proving that a particular NoC is a valid instance of GeNoC, and thus satisfies those correctness theorems, amounts to:

defining the functions that describe the network topology and the access control,
defining all the functions associated with the communications, in particular Routing and Scheduling,
discharging the proof obligations for these functions.

Results

This model has been used to perform formal verification on various communication infrastructures, such as

the Hermes NoC (PUCRS, Brazil),
the Spidergon NoC from STMicroelectronics,
or the Nostrum NoC (Royal Institute of Technology, Stockholm).

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.

We are currently targeting the verification of properties such as deadlock or livelock freedom.

References

A.Helmy: "Mise en oeuvre de techniques de démonstration automatique pour la vérification formelle des NoCs". PhD Thesis, Grenoble University, April 2010 (in French).
A.Helmy, L.Pierre, A.Jantsch: "Theorem Proving Techniques for the Formal Verification of NoC Communications with Non-minimal Adaptive Routing". Proc. IEEE Symposium on Design and Diagnostics of Electronic Systems, Vienna (Austria), April 2010.
D. Borrione, A.Helmy, L.Pierre, J. Schmaltz: "A Formal Approach to the Verification of Networks on Chip". EURASIP Journal on Embedded Systems, 2009.
D. Borrione, A.Helmy, L.Pierre, J. Schmaltz: Chapter "Formal Verification of Communications in Networks-on-Chip". In "Networks-on-Chips: Theory and Practice", F.Gebali and H.Elmiligi editors, CRC Press (Taylor and Francis group), March 2009.
D. Borrione, A.Helmy, L.Pierre, J. Schmaltz: "Executable Formal Specification and Validation of NoC Communication Infrastructures". Proc. 21st Symposium on Integrated Circuits and Systems Design, Gramado (Brazil), September 2008.
J.Schmaltz, D. Borrione: "A functional formalization of on chip communications". Formal Aspects of Computing, 20(3), May 2008.
D. Borrione, A.Helmy, L.Pierre, J. Schmaltz: "A Generic Model for Formally Verifying NoC Communication Architectures: A Case Study". Proc. ACM/IEEE International Symposium on Networks-on-Chips (NoCs'2007), May 2007.
D. Borrione, A.Helmy, L.Pierre: "ACL2-based Verification of the Communications in the Hermes Network on Chip". Proc. IEEE International Workshop on Symbolic Methods and Applications to Circuit Design (SMACD'06), October 2006.
J. Schmaltz, D. Borrione: "A Generic Network on Chip Model". Proc. of 18th International Conference on Theorem Proving in Higher order Logics, August 2005.
J. Schmaltz, D. Borrione: "A Functional Approach to the Formal Specification of Networks on Chip". Proc. FMCAD'04, November 2004.