Murphi2Chisel: A Protocol Compiler from Murphi to Chisel

In distributed systems, modelling and implementing effective coherence protocols is indispensable for resolving issues related to inconsistency. This presents formidable challenges in both modeling and implementing these protocols correctly. This paper introduces Murphi2Chisel, a compiler that establishes connections between the modelling level to implementation level, as well as between event-driven and clock-driven models. The scope of this paper unfolds in two key stages. In the initial phase, a compiler is developed to transform the Murphi-specified coherence protocol into Chisel circuits automatically. Subsequently, we implement a multi-verifying engine for verification of the protocol implementation in Chisel. As a byproduct, we compare the application of various methods involved in both explicit State model checking and symbolic model checking on coherence protocols.