ACL2-based verification of the communications in the hermes network on chip

International audienceMost of today's SOCs (Systems on Chips) are made of manufactured IP's interconnected through complex networks. The IP's have ordinarily been validated by various techniques (simulation, test, formal verification) and the key problem remains the validation of the communication infrastructure. This paper addresses the formal verification of such Networks on Chips by means of a mechanized proof tool, the ACL2 theorem prover. A generic model for NoCs, GeNoC, has been developed and implemented in ACL2. This article proposes an extension of this model to deal with additional features of NoCs and demonstrates the feasibility of our approach on the Hermes network