Formal specification of delta MINs for MPSOC in the ACL2 logic
M. Elleuch, Yassine Aydi, Mohamed Nadhir Abid · 2008
The design of modern multiprocessor systems-on-chip has performance constraints which must be satisfied by the interconnection architecture. multistage interconnection networks, also denoted MINs, seem to be a promising alternative for solving the problems of on-chip communications. This paper presents a formal specification of the Delta multistage interconnection networks for MPSoCs in the ACL2 logic. This work is based on a generic model for networks on chip (GeNoC).