Automated verification of CPU branch-predictors (available)

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. … full description “Automated verification of CPU branch-predictors (available)”

Automated verification of Rowhammer mitigations (available)

Rowhammer [1], first introduced in [2], is a security exploit that relies on electromagnetic side-effects happening in DRAM memories due to repeated accesses to the same row(s) in a short period of time. In fact, accessing the same row in the DRAM many times in a short span of time may cause electromagnetic interactions with … full description “Automated verification of Rowhammer mitigations (available)”