Skip to main content

Modelling and Verification of Interconnects for System-on-Chip Architectures

Start: 1 March 2000
End: 31 May 2003

Project Abstract

This project is an investigation into formal techniques that support the specification and design of on-chip interconnects used in system-on-chip (SOC) architectures. SOCs integrate a number of co-operating modules on a single chip; typically dedicated for a specific domain, e.g. multimedia processing. These modules are linked via a high-speed interconnect which enables interaction; its functional correctness is vital for the whole chip and provides a challenging application for formal design and verification methods. The project focus is on high-level functional modelling with the aim to develop a correct-by-construction refinement and decomposition methodology from a formal system- or transaction-level specification down to signal-level component interfaces.

Summary of Key Advances and Supporting Methodology

The research performed in this project addresses the need for systematic high-level design support for communication protocols used in system-on-chip architectures. Our work concentrated on developing a formal description language and supporting refinement techniques that combine the best of dataflow and process algebras in terms of their expressiveness, compositionality, abstraction power and their well understood refinement relations which provide the basis for high-level system analysis and correct-by-construction component derivation from a single high-level system specification.

The resulting algebra has extensions that allow hierarchical modelling, systematic refinement plus system decomposition, and even the specification of potentially pipelined execution of actions. Its notation is based on process algebraic terms and derivation rules to describe the operational semantics. Support for our algebra has been implemented in a prototype system that is based on FDR.

In more detail, hierarchical modelling utilizes action refinement, where each high-level action and its more detailed refinement establish a new abstraction level. In general, any (high-level) action can be refined by a process that describes in detail what happens while the action is executed. This approach allows to refine a system-level specification of a protocol (eg described at the transaction level) to full signal-level detail without having to specify all implementation specific signals on the system level. System decomposition is based on the dataflow algebraic view of sender and receiver components participating in a communication. By annotating each high-level action in a system model with its sender and receiver components, a function can be defined to formally decompose a so annotated system-level description into concurrent communicating components that adhere to the system-level protocol. In practice, most modern on-chip bus protocols are pipelined to improve the performance of on-chip communication. Pipelining is an implementation technique in which the execution of several actions is overlapped. To support pipelining, we introduced a new operator into our algebra that allows two actions to be overlapped so that an implementation is free to execute the two actions either sequentially or in a pipeline. The corresponding operational rule ensures that pipelining is order preserving with respect to the original action sequence.

Example case studies of our methodology have been performed on the open-source protocols of the PI-bus and parts of the ARM AMBA on-chip bus. The investigated examples demonstrate how interfaces for system components can be derived from a single specification. The interfaces are generated automatically and they bear the same hierarchical structure as the specification. As a consequence, each component of the system can be developed individually using its interface at a different level, thereby allowing the use of partly modelled systems. A further advantage is that the method is modular. In principle, further refinements could be done in the same systematical way. As long as the derivation rules are followed the resulting interfaces are compatible with each other. In that sense, our method is correct-by-construction.

Staff and Students

Kerstin Eder Friedger M?ffke



This project was supported by EPSRC Grant GR/M93758 and a Royal Society Research Equipment Grant.