Formal Verification of a Superscalar Execution Unit

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