Functional verification of a multiple-issue, out-of-order, superscalar Alpha processor---the DEC Alpha 21264 microprocessor