Formal Verification of a Superscalar Execution Unit

Abstract. Many modern systems are designed as a set of interconnected reactive subsystems. The subsystem verification task is to verify an implementation of the subsystem against the simple deterministic high-level specification of the entire system. Our verification methodology, based on Symbolic Trajectory Evaluation, is able e the wide gap between the abstract specification and the implementation specific details of the subsystem. This paper presents a detailed description of an industrial application of this methodology to the fixed point execution unit of the PowerPC processor. We were able to verify a representative instruction under all possible stall, bypass, pipeline conditions and under all possible timings for interface to other functional units in the processor.

• Type: Conference
• Year: 1997
• Where: DAC
• Authors: Kyle L. Nelson, Alok Jain, Randal E. Bryant
• Keywords: Computer Architecture, DAC 1997, Interconnected Reactive Subsystems, Subsystem Verification Task, Symbolic Trajectory Evaluation