|
Abstract : |
Abstract. This is a companion note to Elementary Microarchitecture Algebra [1] and outlines an algebraic simplication proof of the pipelined microarchitecture described in that paper. 1 Transforming the Microarchitecture The laws presented in Elementary Microarchitecture Algebra [1], as well as others introduced in this note, can be used for aggressively restructuring microarchitectures while retaining behavioral equivalence. The example we present here contains three levels of forwarding logic, resolves hazards by stalling the pipeline, and performs branch speculation. The block diagram for this microarchitecture is shown in Figure 1. branch_misp regFile alu mem kill ICache hazard Fig. 1. Microarchitecture before simplication By just using algebraic laws, we have been able to reduce most of the complexity leaving essentially an unpipelined microarchitecture. We have implemented some of the algebraic laws as a rewrite system in Isabelle. The proof proceeds in stages, according to the geometric goal we are pursuing in each stage., |
