Formal verification of Macro-op cache for Arm Cortex-A77, and its successor CPU