Advertisement

Automatic verification of the SCI cache coherence protocol

  • Ulrich Stern
  • David L. Dill
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

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.

Keywords

Reachable State Cache Line Verification System Request Packet Load Instruction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM/IEEE Design Automation Conference, pages 46–51, 1990.Google Scholar
  2. 2.
    D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522–5, 1992.Google Scholar
  3. 3.
    D. L. Dill, S. Park, and A. G. Nowatzyk. Formal specification of abstract memory models. In Symposium on Research on Integrated Systems, pages 38–52, 1993.Google Scholar
  4. 4.
    S. Gjessing, S. Krogdahl, and E. Munthe-Kaas. A top down approach to the formal specification of SCI cache coherence. In Computer Aided Verification. 3rd International Workshop, pages 83–91, 1991.Google Scholar
  5. 5.
    S. Gjessing and E. Munthe-Kaas. Formal specification of cache coherence in a shared memory multiprocessor. Research Report 158, Department of Informatics, University of Oslo, 1991.Google Scholar
  6. 6.
    D. B. Gustavson. The Scalable Coherent Interface and related standards projects. IEEE Micro, 12(1):10–22, 1992.Google Scholar
  7. 7.
    IEEE Std 1596–1992, IEEE Standard for Scalable Coherent Interface (SCI).Google Scholar
  8. 8.
    C. N. Ip and D. L. Dill. Better verification through symmetry. In 11th International Conference on Computer Hardware Description Languages and their Applications, pages 97–111, 1993.Google Scholar
  9. 9.
    C. N. Ip and D. L. Dill. Efficient verification of symmetric concurrent systems. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 230–234, 1993.Google Scholar
  10. 10.
    D. V. James. The Scalable Coherent Interface: Scaling to high-performance systems. In Spring COMPCON, pages 64–71, 1994.Google Scholar
  11. 11.
    D. V. James, A. T. Laundrie, S. Gjessing, and G. S. Sohi. Distributed-directory scheme: Scalable Coherent Interface. Computer, 23(6):74–7, 1990.Google Scholar
  12. 12.
    C. Jard and T. Jéron. Bounded-memory algorithms for verification on-the-fly. In Computer Aided Verification. 3rd International Workshop, pages 192–202, 1991.Google Scholar
  13. 13.
    U. Stern and D. L. Dill. Improved probabilistic verification by hash compaction. In IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 1995.Google Scholar
  14. 14.
    L. Yang, D. Gao, J. Mostoufi, R. Joshi, and P. Loewenstein. System design methodology of UltraSPARCTM-I. In 32nd Design Automation Conference, pages 7–12, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ulrich Stern
    • 1
  • David L. Dill
    • 1
  1. 1.Department of Computer ScienceStanford UniversityStanford

Personalised recommendations