Verifying Deadlock-Freedom for Advanced Interconnect Architectures

Abstract: Modern advanced Interconnects, such as those orchestrated by the ARM AMBA AXI protocol, can have fatal deadlocks in the connection between Masters and Slaves if those transactions are not properly arranged. There exists some research about the deadlock problems in an on-chip bus system and also methods to avoid those deadlocks which could happen. This project aims to verify those situations could make deadlock happens and also the countermeasures for those deadlocks. In this thesis, the ARM AMBA AXI protocol and countermeasures are modelled in NuSMV. Based on these models, we verified the non-trivial cycles of transactions could cause deadlocks and also some bus techniques which can mitigate deadlock problems efficiently. The results from model checking several instances of the protocol and corresponding countermeasures show the techniques could indeed avoid deadlocks.