Abstract
The Delayed Transaction mechanism introduced in version 2.1 of the PCI protocol includes rules for deadlock avoidance which are known to be incomplete in the design community. We have formalized a more complete set of rules as fairness constraints on the behavior of PCI devices and bridges. We present a mathematical proof that these fairness constraints are sufficient to guarantee absence of deadlock for an arbitrary acyclic network of PCI buses, using a novel notion of deadlock-freedom which is generally applicable to any transaction processing system. This verification problem falls outside of the scope of decision procedures based on model checking.
Chapter PDF
Similar content being viewed by others
References
S. Bainbridge, A. Camilleri, and R. Fleming. Theorem proving as an industrial tool for system level design. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem Provers in Circuit Design. North-Holland, 1992.
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the futurebus+ cache coherence protocol. In D. Agnew, L. Claesen, and R. Camposano, editors, Proceedings of the 11th Int. Conf. on Computer Hardware Description Languages and their Applications. North-Holland, 1993.
E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In Computer Aided Verification, 8th International Conference, CAV’96, pages 87–98. Springer-Verlag LNCS 1102, 1996.
M. J. C. Gordon and T. F. Melham. An Introduction to HOL. Cambridge University Press, 1993.
P. H. Ho, Y. Hoskote, T. Kam, M. Khaira, J. O’Leary, X. Zhao, Y. A. Chen, and E. Clarke. Verification of a complete floating-point unit using word-level model checking. In M. Srivas and A. Camilleri, editors, Proceedings of the Int’l Conf. on Formal Methods in Computer-Aided Design, FMCAD’96. Springer-Verlag, November 1996. LNCS 1166.
C. Ip and D. Dill. Better verification through symmetry. In D. Agnew, L. Claesen, and R. Camposano, editors, Proceedings of the 11th Int. Conf. on Computer Hardware Description Languages and their Applications. North-Holland, 1993.
PCI Special Interest Group. PCI Local Bus Specification, Revision 2.1,June 1995.
F. Pong and M. Dubois. A new approach for the verification of cache coherence protocols. IEEE Transactions on Parallel and Distributed Systems, 6 (8): 773–787, August 1995.
Norm Rasmussen. Private communication.
Mandayam K. Srivas and Steven P. Miller. Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Methods in Systems Design, 8(2): 153–188, March 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Corella, F., Shaw, R., Zhang, C. (1997). A formal proof of absence of deadlock for any acyclic network of PCI buses. In: Kloos, C.D., Cerny, E. (eds) Hardware Description Languages and their Applications. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35064-6_15
Download citation
DOI: https://doi.org/10.1007/978-0-387-35064-6_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5387-5
Online ISBN: 978-0-387-35064-6
eBook Packages: Springer Book Archive