Automated verification of CPU branch-predictors (available)

Starting Date: June 2021 (can be flexible)
Duration: 6 weeks
Time commitment: full time
Prerequisites: good knowledge of C and assembly

Branch predictors are components of CPUs that try to guess the outcome of a branching statement (e.g., an if-then-else) before it is known. They speed up the flow of instructions in the instruction pipeline by “pre-executing” what comes after a branching statement, and they play a key role in achieving high performance in modern CPUs.

Flawed branch predictors may lead to serious vulnerabilities. Examples are the recent Spectre and Meltdown, which exploit leftovers of pre-executed instructions in the cache to gain access to private data.

The goal of this project is to develop techniques to automatically verify the correctness of branch predictors. To do this, you will implement known branch predictors (a good overview can be found here [1]), and you will explore the use of the simulation infrastructure [2] to automatically test the correctness of your implementation.

This work will be carried out in the context of the CLeVer (“Verification of Hardware Concurrency via Model Learning”) project, which aims to use AI to reverse-engineer hardware components in order to automatically check their correctness. The CLeVer project is in collaboration with ARM, world-leader in multi-core CPUs design.