Jan. 3, 2001 to Jan. 7, 2001
Siddharth R. Phanse , Tata Institute of Fundamental Research
R.K Shyamasundar , Tata Institute of Fundamental Research
Synchronous languages have been widely used for the reliable design of reactive systems and synchronous circuits as it has become possible to move from the realm of simulations to that of proofs. While Esterel has been used for the modelling and verification of reactive systems, it has not been used that widely for the modelling and verification of cache coherency protocols. In this paper, we shall discuss the use of Esterel for the modelling and verification of cache coherence protocols, in particular on the adaptive cache coherence protocols called Cachet built on the Commit-Reconcile & Fences (CRF) distributed shared memory model. In the paper, we shall (i) first, model the CRF memory model along with the various Cachet micro-protocols in Esterel , (ii) verify properties of the Cachet micro-protocols in a graded manner reflecting the protocol design using the synchronous observer method, and (iii) highlight the experiences in overcoming limitations including state-explosion.
Siddharth R. Phanse, R.K Shyamasundar, "Application of Esterel for Modelling and Verification of Cachet Protocol on CRF Memory Model", VLSID, 2001, VLSI Design, International Conference on, VLSI Design, International Conference on 2001, pp. 179, doi:10.1109/ICVD.2001.902658