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

• Peter Boehm, Oxford University
• Friday 29 October 2010, 13:00-14:00
• Room FW11, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.