Structuring instruction-sets with higher-order functions

In an effort to improve microprocessor performance, each generation of a microprocessor family's instruction-set architecture is typically extended with new features. For example, many modern microprocessors now support parallelism annotations, predication, speculative memory access, and SIMD-based multimedia instructions. These extensions allow a compiler or programmer to directly express instruction-level parallelism that is difficult for the microprocessor to find alone.; This dissertation focuses on the modeling and formal verification of microprocessor designs with instruction-set extensions. Inspired by ARM and IA-64, we develop several elementary instruction-set architectures that employ extensions. We also construct microarchitectural implementation of the instruction sets.; The specification and microarchitectural model in this dissertation are represented in a novel way: as the composition of functions between transition systems. We call these functions transition system transformers. In isolation, transformers can be used to model instruction-set extensions. Together, they can be used to model an entire machine.; This dissertation demonstrates that the extra structure available in transformer-based specifications and models can be used to help decompose a proof that the model implements a specification. We develop several proof strategies that make use of the transformer structure in this way. The contribution of this dissertation is the modeling and verification method that facilitates the decomposition of microarchitectural correctness proofs using instruction-set extensions.