Modern processors are amazing devices: small, fast, low power and getting better with every generation.

But the most amazing things about modern microprocessors is that they work so incredibly reliably despite all their incredible complexity.

This talk is about the battle between complexity and correctness and about how new formal verification tools can be used to help you design higher performance processors that actually work. I will describe the common optimisations, the bugs that these often introduce and how open source tools such as SAT solvers and bounded model checkers can be used to find these bugs.