Abstract

The talk will be split in two parts. First, I present a framework for the incremental modelling and verification of on-chip communication architectures and its application to PCI Express. Arguing formally about the correctness of on-chip communication protocols is an acknowledged verification challenge. Our approach is based on an incremental approach that interleaves model construction and verification. Using abstract building blocks and generic composition rules, models are constructed incrementally by adding protocol features to a parameterised endpoint model. This structured approach controls the model complexity and maintains correctness throughout the modelling process. We show the utility and breadth of the framework by applying it to the PCI Express protocol, a modern, high-performance communication protocol implementing sophisticated features to meet today’s performance demands.

The second part of the talk covers two possible extensions of the work and research visions. The ultimate goal of the presented work is a CAD tool suite in which one is able to specify the required protocol features, and the tool generates a verified architecture model automatically. This model is used to synthesise a reference implementation. As many important protocol functions also run in low-level software, an extension of this research integrates low-level software verification into the methodology. This covers hardware/low-level software co-design and verification including memory models and abstraction levels crossing the hardware-software interface.