Automatic verification of the SCI cache coherence protocol

23Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

This paper describes an ongoing effort to verify the cache coherence protocol of the IEEE/ANSI Standard for Scalable Coherent Interface using the Murφ verification system. A model of the typical set protocol was constructed in the Murφ description language. This model was augmented with a specification of properties necessary for cache coherence. The Murφ verification system automatically checks if all reachable states in the model satisfy the given specification. Although verification is still under way, we have already found several errors in the C-code defining the protocol. Finally, we elucidate the experiences gained in the verification project.

Cite

CITATION STYLE

APA

Stern, U., & Dill, D. L. (1995). Automatic verification of the SCI cache coherence protocol. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 987, pp. 21–34). Springer Verlag. https://doi.org/10.1007/3-540-60385-9_2

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free