Formal Verification of a Pervasive Interconnect Bus System in a High-Performance Microprocessor

In our high-performance powerPC* processor, the correctness of the so-called pervasive interconnect bus system, which provides, among others, test and debug access via external interfaces like JTAG, is of utmost importance. In this paper, we describe our approach informally verifying the correctness of this bus system to combat the coverage problem of simulation-based techniques. The bus system and the associated arbitration logic support several functionalities such as deadlock detection and resolution. In order to efficiently complete all of the required formal analysis for verification, we needed to leverage a variety of proof and semi-formal algorithms, as well as reduction and abstraction algorithms. Experimental results are provided to show the efficiency of this approach