Back in 2005, we did a similar verification of the Y86 processors appearing in the first edition of CS:APP. Our recent work provides an update of both the processor designs and the verification tool.

What did we actually do? The diagram below shows the process by which we constructed a verification model: This model allows us to compare the sequential implementation SEQ to a pipelined implementation PIPE. That is, we can show that for any possible program and any starting state, the two implementations will yield the same results, in terms of their updates to the register file, the condition codes, the program counter, and the memory. In other words, all of the mechanisms in PIPE to deal with data and control hazards—data forwarding, stalling, and exception handling—operate correctly. As the figure illustrates, the HCL control logic descriptions were translated directly into UCLID5 code using a program hcl2U. We have now developed HCL translators to map the control logic into 1) C code for use in a simulator, 2) Verilog code for use by a logic synthesis program, and 3) both the original and most recent versions of UCLID.
UCLID5 makes use of the Z3 SMT solver from Microsoft Research to search for inconsistencies between the two processors. Z3 is a *complete* solver, and so it can determine that no such inconsistency exists, and therefore the design is correct.

A complete report on this effort is available as CMU Technical Report CMU-CS-18-122.