A Framework for Microprocessor Correctness Statements

Abstract Most verifications of out-of-order microprocessors compare state-machine-based implementations and specifications, where the specification is based on the instruction-set architecture. The different efforts use a variety of correctness statements, implementations, and verification approaches. We present a framework for classifying correctness statements about safety that is independent of implementation representation and verification approach. We characterize the relationships between the different statements and illustrate how existing and classical approaches fit within this framework.

• Type: Conference
• Year: 2001
• Where: CHARME
• Authors: Mark Aagaard, Byron Cook, Nancy A. Day, Robert B. Jones
• Keywords: Abstract Most Verifications, CHARME 2001, Correctness Statements, Hardware, State-machine-based Implementations