Abstract--We present a refinement-based compositional framework for showing that pipelined machines satisfy the same safety and liveness properties as their non-pipelined specifica...
ion levels. The framework also supports the generation of test constraints, which can be satisfied using a constraint solver to generate tests. A compositional verification approac...