Formal Verification of Macro-op Cache for Arm Cortex-A77, and its Successor CPU