Hardware Formal Verification at Apple 

18 December 2024 | Sala Stringa | 11:00 | Cristian Mattarei (Apple)  

Abstract

Apple Silicon products pose a massive verification challenge in order to guarantee the required level of quality. In fact, a modern SoC can reach up to 134 billion transistors, and with such a level of complexity formal verification is a crucial technique to achieve this goal.

In this presentation I will give a brief overview of how formal verification is applied at Apple to verify the families of SoC. 

Bio
Cristian Mattarei earned a PhD in formal verification from Fondazione Bruno Kessler in 2016, where his research centered on symbolic model checking based safety and reliability analysis under the supervision of Prof. Alessandro Cimatti. Following his doctoral research, Cristian completed a postdoctoral fellowship at Stanford University with Prof. Clark Barrett, working on SAT and SMT based verification of weak memory models and hardware model checking.

Since 2018, Cristian has been a formal verification engineer at Apple, part of the Silicon Engineering Group. His responsibilities include the verification of the Secure Enclave and the GPU of the Apple Silicon.