Extended Abstract: Formal Specification and Verification of the FM9001 Microprocessor Using the DE System

We present our work on formally specifying and mechanically verifying the correctness of the FM9001 microprocessor design using the DE system. The FM9001 microprocessor design was originally specified and verified in the Nqthm logic by Brock and Hunt using the DUAL-EVAL system, the precursor of DE. The main challenge is that ACL2 does not support Nqthm's shell principle, which is used in the original work to formalize the memory model. Instead we represent a memory cell as a proper list of two elements in which the first element is a flag specifying the memory type of the cell, and the second element is a four-valued vector representing the value of that memory cell. This memory representation does not affect the proof strategy for FM9001 created in the previous work, except for establishing the monotonicity property of a netlist's module, which is part of the FM9001 verification procedure. The reason is because the state approximation notion is changed under our proposed representation of the memory model. By modifying the state approximation definition, we successfully prove that the monotonicity property for a module still holds using stricter hypotheses, and finally prove that the FM9001 microprocessor design is correct with respect to a behavioral specification.