First-order theorem proving based verification of the PCI-X bus architecture

The PCI-X technology was introduced to cope up with the advancement of high performance computing systems by providing the necessary bandwidth and bus performance. However, this increased the testing and verification time because of of the increasing complexity of this bus structure and its interface. Therefore, system level verification can be efficiently used in order to reduce verification time, and hence reduce systems level design flow time. In this paper, we propose to verify the PCI-X bus architecture using Event-B first-order verification method. We provide a system level model for the bus structure and then, formally verify properties related to its operation.