This work reports on the verification of a complex instruction set computer (CISC) processor,named Y86-64, styled after the Intel64 instruction set using the UCLID5 verifier. We developed a methodology in which the control logic is translated into UCLID5 format automatically, and the pipelined processor and the sequential reference version were described with as much modularity as possible. This work provides confidence in the processor designs presented in the Bryant-O'Hallaron textbook on computer systems, and it alsO Provides a case study for the capabilities and performance of UCLID5.

41 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu