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

Plug-n-Play style Intellectual Property(IP) reuse in Sys-tem 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 communica-tion 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 compatibil-ity and component composition and show how our model can be used for compatibility verification, interface synthe-sis 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. 1