This paper delineates a rigorous methodology for microprocessor design verification, and shows how it is promoted by Genesys, an automatic pseudo-random test-program generator. The paper reports on an application of this methodology, using Genesys, to verify an x86 design. The principal contribution of this work is to set the general guidelines for obtaining a compound functional verification framework, and to describe how this can be optimally implemented by a test-program generator such as Genesys. The goal of the paper is to assist in the composition of verification processes which typically include only part of the testing suggested in this framework.