Buffer-oriented microarchitecture verification

Design verification is one of the most difficult and time-consuming tasks in hardware development. The verification problem is exacerbated in processor development due to the ever increasing microarchitecture complexity. The current practice for verifying aggressive microarchitecture mechanisms is accomplished mainly through simulations of user applications and randomly-generated test programs. This is a rather ad hoc approach that leads to unpredictable levels of design coverage. Formal methods offer a viable alternative for verifying smaller components of the microarchitecture but are still unable to handle control complexities present in contemporary speculative and out-of-order microarchitectures.; This dissertation presents a new systematic, simulation-based verification methodology called Buffer-oriented Microarchitecture Verification (BMV). The goal of BMV is to generate high-quality test cases targeted at microarchitecture mechanisms derived from high-level processor specification models. The BMV methodology introduces the concept of buffer-oriented machine partitioning and modeling that provides a new means for representing the microarchitecture of a processor. By focusing on the, information stored in a buffer entry rather than the processor pipeline stages, high-level functionality of key microarchitecture mechanisms can be derived in the form of FSM-like models that accurately describe the status of in-flight instructions.; Based on the BMV-derived models, a technique called Microarchitecture Test Program Generation (MTPG) is introduced for creating effective and efficient instruction sequences targeting the behavior associated with the buffer models. MTPG consists of two phases: high-level test generation and test program translation. Using the conformance testing concept, a number of FSM testing techniques can be employed to obtain high-level tests that verify the microarchitecture. The translation from a high-level test to a test program is automated by the use of small sequences of instructions called atomic sequences that upon execution cause significant microarchitecture events.; The BMV methodology is demonstrated using the PowerPC 604 processor. We empirically show the effectiveness and efficiency of the methodology by comparing the size and coverage of our test programs for different BMW-derived models to those of real user applications and randomly-generated programs. Simulation results show that our test programs achieve higher coverage with far fewer instructions (approximately two orders of magnitude) compared to real and randomly-generated programs. In addition, realistic design errors are used to further evaluate our test programs in the context of design error detection. The simulations of our programs against the types of design errors in the PowerPC 604 indicate that most of the functionality of microarchitecture mechanisms is covered by our test programs. Specifically, 61 out of 63 design errors are detected by our test programs, resulting in 98% error coverage.; Finally, we show how BMV models can be formally used to analyze high-level processor pipeline functionality involving multiple microarchitecture entities. The functionality investigated includes the microarchitecture mechanisms used for determining and handling the three types of inter-instruction dependence, namely data, name, and procedural dependence. Although some of the possible behaviors of the targeted functionality cannot be reasoned through BMV models the majority of the control aspect of processor.