Incremental Modelling and Verification of the PCI Express Transaction Layer
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 w...
| প্রধান লেখক: | |
|---|---|
| বিন্যাস: | Conference item |
| প্রকাশিত: |
IEEE
2009
|
| সংক্ষিপ্ত: | 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. |
|---|