Title :
Incremental modelling and verification of the PCI Express transaction layer
Author_Institution :
Oxford University Computing Laboratory, OX1 3QD, England, UK
Abstract :
PCI Express is a modern, high-performance communication protocol implementing highly sophisticated features to meet today´s performance demands. Although an off-chip protocol, PCI Express implements many principles of future on-chip communication architectures. It is a highly complex protocol which is naturally hard to verify formally. We recently proposed a new methodology, based on a series of model transformation steps, to revise the traditional modelling and verification workflow for designing on-chip protocols. We present the application of the new approach to the PCI Express transaction layer. The work has been accomplished in the Isabelle/HOL theorem prover. By restricting the models to an executable subset of the specification language, we have been able to combine the advantages of specifying in a theorem prover with the advantages of executable models in a functional programming language.
Keywords :
Communication system traffic control; Computer architecture; Concrete; Control systems; Feature extraction; Functional programming; High performance computing; Laboratories; Protocols; Specification languages;
Conference_Titel :
Formal Methods and Models for Co-Design, 2009. MEMOCODE '09. 7th IEEE/ACM International Conference on
Conference_Location :
Cambridge, MA, USA
Print_ISBN :
978-1-4244-4806-7
DOI :
10.1109/MEMCOD.2009.5185376