Modeling and verification of network-on-chip using constrained-DEVS

Verification of models is necessary for some classes of systems to guarantee safety properties in addition to satisfying functional requirements. Exhaustive model checking is a full proof method for verifying lack of undesirable behavior for dynamical systems. In this work, we present a model checking verification method for Network-on-Chip (NoC) models. For this purpose, a constrained version of the atomic DEVS modeling formalism is formulated and applied to verification of an NoC router. This is achieved by adding constraints on the state size and the number of transitions in the atomic model. A model-checker is introduced into the DEVS-Suite simulator for verifying constrained DEVS models using the DEVS simulator protocol. The model-checker is used to verify a model of NoC router component at different scale. The state space size, number of state transitions, and execution time metrics, without and with fault, demonstrate the verification of constrained DEVS models.