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.
We considered seven different variants of the pipeline: the one described in the book, as well as ones that implement various extensions and variations given as homework assignments. All seven were proved correct.
There is really no surprise here, but it's nice to be sure that there's not some subtle bug lingering in our designs.
A complete report on this effort is available as CMU Technical Report CMU-CS-18-122.
