A Case Study on the Verification of Cache Coherence Protocols

M. Azizi, X. Song, and E.-M. Aboulhamid

References

  1. [1] R.K. Gupta, C.N. Coelho, Jr., & G. De Mecheli, Synthesis andsimulation of digital systems containing interacting hardwareand software components, paper presented at 29th DesignAutomation Conference (DAC’92), Anaheim, CA, June 1992.
  2. [2] D.L. Dill, What’s between simulation and formal verification?,paper presented at Design Automation Conference (DAC’98),San Francisco, June 1998.
  3. [3] E.M. Clarke & R.P. Kurshan, Computer-aided verification,IEEE Spectrum, 33 6, 1996, 61–67. doi:10.1109/6.499951
  4. [4] C. Kern & M.R. Greenstreet, Formal verification in hardwaredesign, ACM Trans. on Design Automation of ElectronicSystems (TODAES), 4 (2), 1999, 123–193. doi:10.1145/307988.307989
  5. [5] M. McMillan, Symbolic model checking (Boston: Kluwer,1993).
  6. [6] P. Loewenstein & D.L. Dill, Verification of a multiprocessorcache protocol using simulation relations and high-order logic,Proc. 2 nd Int. Workshop on Computer Aided Verification,New Brunswick, NJ, June 1990, 302–311.
  7. [7] M. Gordon & T. Melham, Introduction to HOL: A theoremproving environment for higher order logic (Cambridge: Cambridge University Press, 1993).
  8. [8] R. Nalumaru, R. Ghughal, A. Mokkedem, & G. Gopalakrishnan, The “test model checking approach to the verificationof formal memory models of multiprocessors, Technical reportUUCS-98-008, University of Utah, Salt Lake City, UT, 1998.
  9. [9] E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long,K.L. McMillan, & L.A. Ness, Verification of the Futurebus+cache coherence protocol, Proc. 11 th Int. Symp. on Computer Hardware Description Languages and Their Applications (CHDL ’93), Ottawa, April 1993.
  10. [10] K.L. McMillan & J. Schwalbe, Formal verification of thegigamax cache consistency protocol, Proc. Int. Symp. on SharedMemory Multiprocessors, Tokyo, Japan, April 1991, 242–251.9
  11. [11] X.S. Li, A. Cau, B.C. Moszkowski, N. Coleman, & H. Zedan,Proving the correctness of the Interlock Mechanism in ProcessorDesign, paper presented at CHARME ’97, 105, Montreal, QC,October 1997.
  12. [12] N. Narasimhan, R. Kalyanaraman, & R. Vemuri, Validationof synthesized RTL designs using simulation and formal verification, paper presented at HLDVT Workshop, Oakland, CA, November 1996.
  13. [13] F. Pong & M. Dubois, A new approach for the verificationof cache coherence protocols, IEEE Trans. on Parallel andDistributed Systems, 6 (8), 1995, 773–787. doi:10.1109/71.406955
  14. [14] F. Pong, Symbolic state model: A new approach for the verification of cache coherence protocols, doctoral diss., Department of Electrical Engineering—Systems, University of Southern California, August 1995.
  15. [15] M. Azizi, O. Ait-Mohamed, & X. Song, Cache coherenceprotocol verification for a multiprocessor system with sharedmemory, Proc. 10 th Int. Conf. on Microelectronics (ICM ’98),Monastir, Tunisia, December 1998, 99–102. doi:10.1109/ICM.1998.825578
  16. [16] F. Pong & M. Dubois, A survey of verification techniques forcache coherence protocols, ACM Computing Surveys, 29 (1),1997, 11–20. doi:10.1145/248621.248624
  17. [17] J. Archibald & J.L. Baer, Cache coherence protocols: Evaluation using a multiprocessor simulation model, ACM Trans. on Computer Systems, 4 (4), 1986, 273–298. doi:10.1145/6513.6514
  18. [18] J.L. Baer & C. Girault, A Petri net model for a solution to thecache coherence problem, Proc. 1 st Conf. on SupercomputingSystems, Washington, DC, 1985, 680–689.
  19. [19] G.V. Bochmann & C.A. Sunshine, Formal methods in communication protocol design, IEEE Trans. on Communications, COM-28 (4), 1980, 624–631. doi:10.1109/TCOM.1980.1094685
  20. [20] L.M. Censier & P. Feautrier, A new solution to coherenceproblems in multicache systems, IEEE Trans. on Computers,C-27 (12), 1978, 1112–1118. doi:10.1109/TC.1978.1675013
  21. [21] P. Stenstrom, A survey of cache coherence schemes for multi-processors, IEEE Computer, 23 (6), 1990, 12–24. doi:10.1109/2.55497
  22. [22] S. Graf, Verification of a distributed cache memory by usingabstractions, Proc. 6 th Int. Workshop on Computer-AidedVerification, Stanford, CA, 1994, 207–219.
  23. [23] W.C. Yen, W.L. Yen, & K.S. Fu, Data coherence problem ina multi-cache system, IEEE Trans. on Computers, C-34 (1),1985, 56–65. doi:10.1109/TC.1985.1676515
  24. [24] M.C. Yuang, Survey of protocol verification techniques basedon finite state machine models, Proc. Computer NetworkingSymp., Washington, DC, April 1988, 164–172. doi:10.1109/CNS.1988.4993
  25. [25] VIS Home Page: http://www.berkely.edu/vis/.
  26. [26] R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F.Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y.Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R.Shiple, G. Swamy, & T. Villa, VIS: A system for verificationand synthesis, Technical report UCB/ERL M95, Electron-ics Research Laboratory, University of California, Berkeley,December 1995.
  27. [27] FormalCheck v2.1, Lucent Technologies, 1998.
  28. [28] D.A. Patterson & J.L. Hennessy, Computer organization anddesign: The hardware/software interface (Morgan Kaufmann,1994).
  29. [29] R.W. Hartenstein, Hardware description languages: Advancesin CAD for VLSI, Vol. 7 (Elsevier, 1987).
  30. [30] K.L. McMillan, Symbolic model checking: An approach tothe state explosion problem, doctoral diss., Carnegie-MellonUniversity, Pittsburgh, 1992.
  31. [31] K.L. McMillan, Parameterized verification of the FLASH cachecoherence protocol by compositional model checking, paperpresented at CHARME 2001, Livingston, Scotland, September2001, 179–195.
  32. [32] F. Pong & M. Dubois, Formal automatic verification of cache coherence in multiprocessors with relaxed memory models, IEEE Trans. on Parallel and Distributed Systems, 11(9), 2000, 989-1006 doi:10.1109/71.879780

Important Links:

Go Back