– 31 – FLoC 06 Verifying OOO Lahiri, Seshia, & Bryant, FMCAD 2002Goal Show that OOO implements Instruction Set Architecture (ISA) model For all possible execution sequencesChallenge OOO holds partially executed instructions in reorder buffer States of two systems match only when reorder buffer flushed ISA Reg.
{}