Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem

The transaction ordering problem of the original PCI 2.1 standard bus specification violates the desired correctness property of maintaining the so called Producer/Consumer relationship between writers and readers of data. This violation stems mainly from the so called completion stealing problem, first identified and solved by Corella et al. 4], and supported by a formal paper and pencil argument. In this paper, we develop a flexible graph theory library in PVS for modeling computer bus structures, formalize the PCI 2.1 protocol containing the solution of 4] in it, and mechanically prove the absence of completion stealing. Next, we define the Producer/Consumer property in PVS and sketch its mechanical proof. Noting the complexity of this proof effort (unfinished as yet), we explore a combination of theorem proving and model-checking in which the model used for model-checking is made tractable by exploiting the formal theorems established during theorem-proving as well as several intuitively justified assumptions. The theorem-proving infrastructure we have built for modeling CPU interconnect structures is highly reusable. Our work is one example of a natural division of labor between theorem-proving and model-checking in tackling system-level verification problems under realistic time budgets.