Cache coherence protocols serve as the cornerstone for ensuring data consistency in multi-core systems and directly impact the performance of the memory subsystem,making it a longstanding focal point in microprocessor design and verification.The design and optimization of coherence protocols typically rely on software simulators like gem5 for rapid implementation.Additionally,errors in protocols are difficult to trigger,locate,and repair during simulation,necessitating the use of model checking tools such as Murphi for formal verification.However,there is a significant difference in programming languages and levels of abstraction between simulator-based protocol design and optimization and model-checking-based protocol verification.Designers are required to separately implement simulator code and construct model-checking frameworks,which not only increases time cost but also introduces potential discrepancies in equivalence between the two approaches.To address this challenge,this paper designs and implements Rubyphi,an automated model checking method for Cache coherence protocols targeting the gem5 simulator.By extracting and translating the protocol descriptions and implementations from gem5,Rubyphi automatically generates Murphi-based model checking framework to conduct formal verification.Experimental results demonstrate that Rubyphi effectively accomplishes the modeling and verification of coherence protocols in gem5,successfully uncovering two existing bugs in gem5 s protocols.The related issues and patches have been confirmed  by the community.