Digital's Alpha-based DECchip 21164 processor was verified extensively prior to fabrication of silicon. This simulation-based verification effort used implementation-directed, pseudorandom exercisers which were supplemented with implementationspecific, hand-generated tests. Special emphasis was placed on the tasks of checking for correct operation and functional coverage analysis. Coverage analysis shows where testing is incomplete, under the assumption that untested logic often contains bugs. Correctness checkers are various mechanisms (both during and after simulation) that monitor a test to determine if it was successful. This paper details the coverage analysis and correctness checking techniques that were used. We show how our methodology and its implementation was successful, and we discuss the reasons why this methodology allowed several minor bugs to escape detection until the first prototype systems were available. These bugs were corrected before any chips were shipped to customers.