Synchronous protocol automata: a framework for modelling and verification of SoC communication architectures

Plug-n-Play style Intellectual Property (IP) reuse in System on Chip (SoC) design is facilitated by the use of an on-chip bus architecture. We present a synchronous, Finite State Machine based framework for modelling communication aspects of such architectures. This formalism has been developed via interaction with designers and the industry and is intuitive and lightweight. We have developed cycle accurate methods to formally specify protocol compatibility and component composition and show how our model can be used for compatibility verification, interface synthesis and model checking with automated specification. We demonstrate the utility of our framework by modelling the AMBA bus architecture including details such as pipelined operation, burst and split transfers, the AHB-APB bridge and arbitration features.