Term-Level Verification of a Pipelined CISC Microprocessor

By abstracting the details of the data representations and operations in a microprocessor, term-level verification can formally prove that a pipelined microprocessor faithfully implements its sequential, instruction-set architecture specification. Previous efforts in this area have focused on reduced instruction set computer (RISC) and very-large instruction word (VLIW) processors. This work reports on the verification of a complex instruction set computer (CISC) processor styled after the Intel IA32 instruction set using the UCLID term-level verifier. Unlike many case studies for term-level verification, this processor was not designed specifically for formal verification. In addition, most of the control logic was given in a simplified hardware description language. We developed a methodology in which the control logic is translated into UCLID format automatically, and the pipelined processor and the sequential reference version were described with as much modularity as possible. The latter feature was made especially difficult by UCLID’s limited support for modularity. A key objective of this case study was to understand the strengths and weaknesses of UCLID for describing hardware designs and for supporting the formal verification process. Although ultimately successful, we identified several ways in which UCLID could be improved.