Hardware Verification and Proving Very Large Theorems

I will give a survey of microprocessor verification work in
which I have participated using the NQTHM and the ACL2
theorem provers, and I will describe which pieces were used
in the CLI verified stack. I will also discuss the hardware
verification tools I helped develop at IBM. This survey
begins in the 1980\\\'s and will provide a general
introduction to microprocessor verification. I will briefly
discuss the verification of the FM8501, FM8502, and
Motorola\\\'s CAP DSP. I will describe the verification of
the FM9001 microprocessor, which served as the foundation
for the CLI verified stack. I will describe the FM9801
microprocessor verification, and, time permitting, I will
summarize array verification. I will close with some
discussion about future hardware verification topics.