This paper describes Hopscotch, a novel flow-graph based scalable framework used to formally specify and verify a complex RTL implementation of Arm v8.5 Memory Tagging Extension (MTE) functionality on the Load-Store unit of a high-performance Arm CPU. It also describes the implementation details of a Store Execution Checker built on this framework, a summary of results, limitations and future improvements.