A functional specification and validation model for networks on chip in the ACL2 logic

International audience

We present a functional model used to specify and validate, in the ACL2 logic, a system on a chip communication architecture named Octagon. The functional model is briey introduced before being developed on the case study. We define and validate the routing algorithm, a simple scheduling algorithm and the correctness of read and write operations which includes the proof that messages travel over the network without being modified and eventually reach their expected destination.