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 specification to seemingly looser, multi-step, criteria. In this paper, we formally verify conditions under which two categories of multi-step correctness statements logically imply single-step correctness statements. The first category of correctness statements compare flushed states of the implementation and the second category compare states that are able to retire instructions. Our results are applicable to superscalar implementations, which fetch or retire multiple instructions in a single step.
Cite
CITATION STYLE
Aagaard, M. D., Day, N. A., & Lou, M. (2002). Relating multi-step and single-step microprocessor correctness statements. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2517, pp. 123–141). Springer Verlag. https://doi.org/10.1007/3-540-36126-x_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
