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.