Formal Verification of NoCs: The GeNoC Approach

 

Julien Schmaltz (Radboud University, Nijmegen, NL)

 

Abstract:

 

 In a near future, computing systems -- embedded in small devices or
laptops -- will all be multi-core chips. In this context, the design
challenges lie in (1) raising the level of abstraction of the initial
design phase while maintaining the link with the final Register
Transfer Level (RTL) implementation, and (2) the correctness and the
performance of the communication architecture. Ideally,
Systems-on-Chips result from the integration of parameterized
components. Moreover, the traditional bus architecture is no more
adequate. Complex Networks-on-Chips (NoCs) are required.

  GeNoC is a generic network model unifying communication
architectures at a high-level of abstraction. This model embraces
protocols, routing algorithms and switching techniques. It identifies
the key constituents common to all communication architectures, and
their essential properties from which the correctness of the overall
model is deduced. Thus, the verification of any particular design is
reduced to the proof of the essential properties. GeNoC has been
expressed in the logic of the ACL2 theorem proving system. The ACL2
GeNoC model has been applied to several architectures that constitute
concrete instances of GeNoC.

  In this talk, I will present the current status of the GeNoC
approach, some of its applications, and conclude with the presentation
of on-going developments at Radboud University Nijmegen: (1) adding
deadlock avoidance and performance properties to the abstract
specification model, and (2) defining refined models to relate
specifications to concrete RTL implementations.