@inproceedings{76feb1e2b25942029641fc7ede694164,
title = "Murphi2Chisel: A Protocol Compiler from Murphi to Chisel",
abstract = "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.",
keywords = "Chisel, Coherence protocol, Explicit state model check, Murphi, Symbolic model check",
author = "Zhenghai Cai and Yongjian Li and Yongxin Zhao",
note = "Publisher Copyright: {\textcopyright} 2024 Owner/Author.; 15th Asia-Pacific Symposium on Internetware, Internetware 2024 ; Conference date: 24-07-2024 Through 26-07-2024",
year = "2024",
month = jul,
day = "24",
doi = "10.1145/3671016.3671376",
language = "英语",
series = "ACM International Conference Proceeding Series",
publisher = "Association for Computing Machinery",
pages = "209--218",
booktitle = "15th Asia-Pacific Symposium on Internetware, Internetware 2024 - Proceedings",
address = "美国",
}