A complete compositional reasoning framework for the efficient verification of pipelined machines

We present a compositional reasoning framework based on refinement for verifying that pipelined machines satisfy the same safety and liveness properties as their instruction set architectures. Our framework consists of a set of convenient, easily-applicable, and complete compositional proof rules. We show that our framework greatly extends the applicability of decision procedures by verifying a complex, deeply pipelined machine that state-of-the-art tools cannot currently handle. We discuss how our framework can be added to the design cycle and highlight what arguably is the most important benefit of our approach over current methods, that the counterexamples generated are much simpler, as bugs are isolated to a particular step in the composition proof.