Formal Verification of the Communications in Networks on Chips

Abstract. Most of today's SoC's (Systems on Chips) are made of manufactured IP's interconnected through complex networks on chips (NoCs). We propose a generic NoC model, GeNoC, as a formal reference for the specification, formal verification, and simulation at the initial design phase. The model is implemented by means of a mechanized proof tool, the ACL2 theorem prover, and is used to formally verify instances of NoCs