Abstract:RCC cache coherence protocol in Godson-T many-core processor is a characteristic parameterized concurrent system. It is a challenge to verify this protocol. Cubicle is a recently built parameterized model checking tool based on SMT solver. We used Cubicle to model and verify RCC protocol successfully. The experimental results show that RCC protocol satisfies all kinds of safety properties regardless of how many nodes it has.