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.

The FM9801 microprocessor has been formally described with an abstract ISA specification and a micro-architectural implementation. These specifications were written in the ACL2 logic, and a proof that the micro-architectural implementation satisfies its ISA-level specification was mechanically checked using the ACL2 theorem-proving system. I will present the correctness diagram used to state this correctness result, exhibit some invariants that were proven, and present some results of this effort.

Many contemporary hardware designs now contain more transistors of memory arrays than of logic. To ensure that arrays are correctly implemented requires analysis of their transistor-level implementations. Modern array designs are much more sophisticated than just simple memories, as they include priority encoders, multiple read and write ports, content-addressable memory, and random logic. I will give an example array verification, and describe an array verification tool that I helped develop.

I will mention a few research problems I see approaching in the hardware verification field. These involve both the expansion of hardware verification techniques along with the fusion of additional modeling requirements.