Politecnico di Torino (logo)

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

Leonardo Bellettini

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

Rel. Maurizio Martina. Politecnico di Torino, Corso di laurea magistrale in Ingegneria Elettronica (Electronic Engineering), 2021


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.

Relators: Maurizio Martina
Academic year: 2020/21
Publication type: Electronic
Number of Pages: 105
Additional Information: Tesi secretata. Fulltext non presente
Corso di laurea: Corso di laurea magistrale in Ingegneria Elettronica (Electronic Engineering)
Classe di laurea: New organization > Master science > LM-29 - ELECTRONIC ENGINEERING
Aziende collaboratrici: Arm Cambridge
URI: http://webthesis.biblio.polito.it/id/eprint/17960
Modify record (reserved for operators) Modify record (reserved for operators)