Deadlock is a historically well-known bug pattern in computer systems where, in the most general sense, a system reaches a state in which it cannot progress any further. In this work, we investigate deadlocks in packet switching networks with a deterministic routing function. We formalize three different notions of deadlock, namely, global, local and weak deadlock. We formally define the relation between these different notions. Moreover, we formalize packet switching networks in nuXmv and verify them for each of the notions of deadlock, based on the theory proposed. We also explore the translation of these networks to xMAS.