Title: 

  Modelling and verification with synchronous protocol automata

Speaker: S. Ramesh, GM R&D Bangalore and IIT Bombay


Abstract:

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.
Component integration and verification in such systems is a cumbersome
and time consuming process largely concerned with interfacing
related issues. 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 light weight. We have developed cycle
accurate methods which can be used for protocol specification, compatibility
verification, interface synthesis and model checking with automated
specification. The case studies we performed include the AMBA family of
protocols and a proprietary industrial bus protocol. Our experience has
shown that our models enable reasoning about and comparison of dierent
bus architectures to gain valuable design insights. We demonstrate
the utility of our framework by modelling the AMBA bus architecture
including details such as pipelined operation, burst transfers, the AHBAPB
bridge and arbitration features.