University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A Framework for Incremental Modelling and Verification of On-Chip Protocols and Its Application to PCI Express

A Framework for Incremental Modelling and Verification of On-Chip Protocols and Its Application to PCI Express

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Bjarki Holm.

Note the unusual time (13:00)

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity