L1 Memory System Formal Verification of a Cortex-R class CPU at Arm

Formal Verification (FV) refers to the use of static analysis methods to verify a design. Within Arm, I have mostly used a technique known as model checking, in which requirements of a design are expressed in a formal mathematical language (usually SystemVerilog Assertions), and tools are used to analyse whether there is any way that a given model of the design can fail to satisfy the requirements. FV is a static testing, differently from simulation, and it doesn't require any stimulus. The big advantage of FV is that it can give exhaustive proofs, meaning that the written property is always true for all the possible cases. Arm Cortex-R real-time processors offer high-performance computing solutions for embedded systems where reliability, high availability, fault tolerance and/or deterministic real-time responses are needed. Cortex-R processors are used in products where performance requirements and timing deadlines must always be met. In this thesis I will present my work done in the formal verification team at Arm in Cambridge, England. My role was to apply formal verification to verify the L1 Memory System of the latest Cortex-R class CPU still under development. Many techniques have been used and I worked on many different units, so this thesis will show how Formal Verification can be useful to find very hidden bugs that the classic simulation approach would not be able to find.