Portal de Periódicos da CAPES

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

1998; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-49519-3_17

1611-3349

Abdel Mokkedem, Ravi Hosabettu, Ganesh Gopalakrishnan,

Embedded Systems Design Techniques

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. In [3], a correction to this ordering problem was proposed and informally proved (called the "HP solution" here). In this paper, we present a formalization of the PCI 2.1 protocol in PVS. We formalize the fact that with Local Master ID added to the protocol no completion stealing is possible and the Producer/Consumer property is provided even in the presence of multiple readers. The state of our proofs leading to this result, as well as some of the much needed enhancements to theorem-proving frameworks that will greatly facilitate similar proofs, are also elaborated.