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

Plug-n-play-style intellectual property reuse in system-on-chip design is facilitated by the use of an on-chip bus architecture. Component integration and verification in such systems is a cumbersome and time consuming process largely concerned with interfacing issues. A synchronous, finite state machine framework for modelling communication aspects of such architecture is presented. The framework has been developed via interaction with designers and the industry, and is intuitive and light-weight. The development includes cycle-accurate methods for protocol specification, compatibility verification, interface synthesis and model checking with automated specification. Case studies performed include the AMBA family of protocols and a proprietary industrial bus protocol. These modelling exercises show that such models enable reasoning about and comparison of different bus architectures to gain valuable design insights. The utility of this framework is demonstrated by modelling the AMBA bus architecture including details such as pipelined operation, burst transfers, the AHB-APB bridge and arbitration features.