Mothers of Pipelines

We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set architecture (ISA). The MOP vs. ISA correctness theorem splits naturally into a large number of simple subgoals. This theorem reduces proving the correctness of a given pipelined implementation of the ISA to verifying that each of its transitions can be modeled as a sequence of MOP state transitions.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Sava Krstic, Robert B. Jones, John O'Leary
• Keywords: ENTCS 2007, ISA Correctness, Pipeline Verification, SMT Solvers