Formal Verification of a Snoop-Based Cache Coherence Protocol Using Symbolic Model Checking

Srivatsan Srinivasan; Adnan Aziz; Lizy John; Parminder Singh Chhabra; Praveen Kumar Jaini

doi:10.1109/ICVD.1999.745162

V
VLSID
1999
12th International Conference on VLSI Design - 'VLSI for the Information Appliance'
Abstract - Formal Verification of a Snoop-Based Cache Coherence Protocol Using Symbolic Model Checking

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/EndNote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Srivatsan Srinivasan Articles by Parminder Singh Chhabra Articles by Praveen Kumar Jaini Articles by Adnan Aziz Articles by Lizy John

12th International Conference on VLSI Design - 'VLSI for the Information Appliance'

Formal Verification of a Snoop-Based Cache Coherence Protocol Using Symbolic Model Checking

Goa, India

January 10-January 13

ISBN: 0-7695-0013-7

	ASCII Text	x
	Srivatsan Srinivasan, Parminder Singh Chhabra, Praveen Kumar Jaini, Adnan Aziz, Lizy John, "Formal Verification of a Snoop-Based Cache Coherence Protocol Using Symbolic Model Checking," VLSI Design, International Conference on, pp. 288, 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', 1999.

	BibTex	x
	@article{ 10.1109/ICVD.1999.745162, author = {Srivatsan Srinivasan and Parminder Singh Chhabra and Praveen Kumar Jaini and Adnan Aziz and Lizy John}, title = {Formal Verification of a Snoop-Based Cache Coherence Protocol Using Symbolic Model Checking}, journal ={VLSI Design, International Conference on}, volume = {0}, year = {1999}, issn = {1063-9667}, pages = {288}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICVD.1999.745162}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - VLSI Design, International Conference on TI - Formal Verification of a Snoop-Based Cache Coherence Protocol Using Symbolic Model Checking SN - 1063-9667 SP EP A1 - Srivatsan Srinivasan, A1 - Parminder Singh Chhabra, A1 - Praveen Kumar Jaini, A1 - Adnan Aziz, A1 - Lizy John, PY - 1999 VL - 0 JA - VLSI Design, International Conference on ER -

Srivatsan Srinivasan, The University of Texas at Austin

Parminder Singh Chhabra, The University of Texas at Austin

Praveen Kumar Jaini, The University of Texas at Austin

Adnan Aziz, The University of Texas at Austin

Lizy John, The University of Texas at Austin

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICVD.1999.745162

Formal verification of cache coherence in a multiprocessor environment is essential in ascertaining the validity of a cache coherence protocol. Although a number of cache coherence verification techniques are available, very few authors have reported results on verification of cache coherence protocols using symbolic model checking. In this paper we present the verification of a three state snoopbased cache coherence protocol using model checking in VIS. As symbolic model checking is beset with the state explosion problem, directly verifying the protocol for large number of processors is infeasible. We have developed a set of modeling strategies that we found useful in verifying cache coherence of two to five processor configurations. In this paper, we report the techniques we adopted in modeling and verifying the protocol.

Citation:

Srivatsan Srinivasan, Parminder Singh Chhabra, Praveen Kumar Jaini, Adnan Aziz, Lizy John, "Formal Verification of a Snoop-Based Cache Coherence Protocol Using Symbolic Model Checking," vlsid, pp.288, 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', 1999

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.