[Gems-users] Formal Verification of Cache Coherence Protocols

[Abdullah Kayi <apokayi@xxxxxxxxxxxxxx>]

Hi all,

I modified some of the GEMS released protocols and I am looking for a 
possible way of doing formal verification. I read the CAN' 2005 GEMS 
paper and I saw couple of sentences talking about this, specifically 
converting SLICC codes to TLA+ or Murphi. I was wondering whether there 
is any automated tool available for this purpose as of now. Or, if 
anybody has tried this before, can I get some tips on how to proceed?
Thanks in advance,

Abdullah