Hopscotch: A Scalable Flow-Graph Based Approach to Formally Specify and Verify Memory-Tagged Store Execution in Arm CPUs

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.

Vikram Khosa, Arm
Sai Komaravelli, Arm
Madhu Iyer, Arm
Abhinav Sethi, Arm