Theorem proving techniques for the formal verification of NoC communications with non-minimal adaptive routing

This paper focuses on the formal verification of communications in Networks on Chip. We describe how an enhanced version of the GeNoC proof methodology has been applied to the Nostrum NoC which encompasses various non-trivial features such as a deflective non-minimal routing algorithm. We demonstrate how the features of the Nostrum protocol layers can be captured by the current version of GeNoC that enables a step-by-step formalization of communication operations while taking various protocol details into consideration. We prove that packets arrive properly and that packets are never lost. Also, we prove the soundness of the Nostrum data link, network and transport layers.