System level Modeling and Verification of NoC Components using model checking


Prof. Sowmya Arcot , School of Computer Science and Engineering (UNSW) Sydney, Australia

16.06.2014, 11:00, room 4981


Network on chip (NoC) is a system design methodology that uses on-chip routers for integrating the resources on a system on chip (SoC). Applications on the SoC communicate through a layered communication protocol implemented on the NoC’s router-based communication architecture. There is need for a formal system level model of NoC to verify end-to- end protocol correctness in an NoC architecture. In this work, we present a new formal model of the existing Hermes NoC router architecture and its communication scheme using a new formal language called Heterogeneous Protocol Automata (HPA). HPA models the five bi-directional ports and the bounded buffers at input port of the Hermes Router including the XY routing algorithm, the priority based arbitration logic, wormhole switching and the request-ack handshake protocol of the communication scheme. The automata model is mapped manually in PROMELA, the specification language of the SPIN model checker for verification.


Arcot Sowmya holds the position of Professor of Computer Science and Engineering, University of New South Wales, Sydney, Australia. Her interests in formal modelling, design and verification of embedded systems span Real-time, Concurrent and Embedded systems: modelling, specification and verification techniques, components-based design tools, adaptive reuse in embedded system design, electronic design automation and embedded real-time software design.