BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Framework for Incremental Modelling and Verification of On-Chip 
 Protocols and Its Application to PCI Express - Peter Boehm\, Oxford Univer
 sity
DTSTART:20101029T120000Z
DTEND:20101029T130000Z
UID:TALK27756@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:The talk will be split in two parts. First\, I present a frame
 work for the incremental modelling and verification of on-chip communicati
 on architectures and its application to PCI Express. Arguing formally abou
 t the correctness of on-chip communication protocols is an acknowledged ve
 rification challenge. Our approach is based on an incremental approach tha
 t interleaves model construction and verification. Using abstract building
  blocks and generic composition rules\, models are constructed incremental
 ly by adding protocol features to a parameterised endpoint model. This str
 uctured approach controls the model complexity and maintains correctness t
 hroughout the modelling process. We show the utility and breadth of the fr
 amework by applying it to the PCI Express protocol\, a modern\, high-perfo
 rmance communication protocol implementing sophisticated features to meet 
 today's performance demands.\n\nThe second part of the talk covers two pos
 sible extensions of the work and research visions. The ultimate goal of th
 e presented work is a CAD tool suite in which one is able to specify the r
 equired protocol features\, and the tool generates a verified architecture
  model automatically. This model is used to synthesise a reference impleme
 ntation. As many important protocol functions also run in low-level softwa
 re\, an extension of this research integrates low-level software verificat
 ion into the methodology. This covers hardware/low-level software co-desig
 n and verification including memory models and abstraction levels crossing
  the hardware-software interface.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR