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)”