These cache coherence protocols were designed from scratch and implemented in Murphi for EECS 570. Correctness was verified for up to three sharers on a single cache block, and the implementation assumes an unordered network.
Disclaimer: Functionality and simplicity were my only goals for the project (since we weren't graded on performance), and so my design will be horribly inefficient in practice and has more virtual channels and transient states than necessary.
The designs for MSI and MESI are shown below, with red states highlighting differences from the (ordered network) baseline described in Sorin et al's "A Primer on Memory Consistency and Cache Coherence".
MSI:
