Formal methodology for modeling, verifying and optimizing reconfigurable NoC modes

摘要

The paper proposes a formal verification process for reconfigurable Network-on-chip in MPSoC. The reconfiguration of the MPSoC can lead to the addition of messages that can create an overload on the NoC and violate the deadline of messages that have to be routed. We present an adaptive routing algorithm for this case able to adapt himself to this overload. When the NoC is no more able to support the overload, it is reconfigured to route only the most important messages on a (m, k) basis. On the other hand, the overload can lead also to an over consumption of the energy available. Again, the solution is a reconfiguration of the NoC to move to an (m, k) routing. We propose for all these scenarios a formal verification process using Reconfigurable Timed Net Condition/Event Systems (R-TNCES) model to support the reconfiguration. The temporal and functional properties are verified using the model checker SESA.