Verification of executable pipelined machines with bit-level interfaces

We show how to verify pipelined machine models with bit-level interfaces by using a combination of deductive reasoning and decision procedures. While decision procedures such as those implemented in UCLID can be used to verify pipelined machines, the models are at the term level: they abstract away the datapath, require the use of numerous abstractions, implement a small subset of the instruction set, and are far from executable. In contrast, we focus on verifying executable machines with bit-level interfaces. Such proofs have previously required substantial expert guidance and the use of deductive reasoning engines. We show that by integrating UCLID with the ACL2 theorem proving system, we can use ACL2 to reduce the proof that an executable, bit-level machine refines its instruction set architecture to a proof that a term level abstraction of the bit-level machine refines the instruction set architecture, which is then handled automatically by UCLID. In this way, we exploit the strengths of ACL2 and UCLID to prove theorems that are not possible to even state using UCLID and that would require prohibitively more effort using just ACL2.