Re: [Gems-users] Formal Verification of Cache Coherence Protocols

[Polina Dudnik <pdudnik@xxxxxxxxx>]

Hi Abdullah,

Currently we are not aware of any tools out there to perform formal verification. In general we verify the protocols through rigorous testing. You might find this paper interesting "Verifying a Multiprocessor Cache Controller Using Random Test Generation". 

Maybe someone else on the list can comment on this?

Polina

On Fri, May 29, 2009 at 6:49 PM, Abdullah Kayi <apokayi@xxxxxxxxxxxxxx> wrote:

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
_______________________________________________
Gems-users mailing list
Gems-users@xxxxxxxxxxx
https://lists.cs.wisc.edu/mailman/listinfo/gems-users
Use Google to search the GEMS Users mailing list by adding "site:https://lists.cs.wisc.edu/archive/gems-users/" to your search.