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. The authors 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. They 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. They prove that packets arrive properly and that packets are never lost. Also, they prove the soundness of the Nostrum data link, network and transport layers.