Relating multi-step and singlestep microprocessor correctness statements

Abstract. A diverse collection of correctness statements have been proposed and used in microprocessor verification efforts. Correctness statements have evolved from criteria that match a single step of the implementation against the specifi-cation to seemingly looser, multi-step, criteria. In this paper, we formally verify conditions under which two categories of multi-step correctness statements log