Incremental Modelling and Verification of the PCI Express Transaction Layer
Peter Böhm
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.
Details
| Book Title |
Proceedings of the Seventh ACM−IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'09) |
| ISBN |
978−1−4244−4807−4 |
| Location |
Cambridge‚ MA‚ USA |
| Month |
July |
| Pages |
36–45 |
| Publisher |
IEEE Computer Society |
| Year |
2009 |
Links
DOI (10.1109/MEMCOD.2009.5185376)
Related pages
|
People |
|
|
Projects |
Verified Communication Protocols for Multicore/SoC Architectures |