Global Microprocessor Correctness in the Presence of Transient Execution

Correctness for microprocessors is generally understood to be conformance with the associated instruction set architecture ISA. This is the basis for one of the most important abstractions in computer science, allowing hardware designers to develop highly-optimized processors that are functionall...