A re-use methodology for formal SoC protocol compliance verification

We propose a new methodology for formally specifying on-chip bus protocols and for verifying protocol compliance of communication blocks in System-on-Chip (SoC) designs. In this methodology, the bus protocol is specified in a design-independent way by a set of protocol compliance properties based on a generic recorder finite state transition system. The properties are verified by combining local reachability analysis with a SAT-based property checking approach. This approach is called interval property checking and is based on a bounded circuit model generated from the design and the recorder. The proposed methodology clearly differentiates between design-specific and protocol-specific aspects of the overall verification task and exploits the nature of typical SoC protocol specifications and implementations. In this way, the proposed methodology contributes to reaching two important goals: making the computational complexity of formal verification algorithms tractable for large designs and reducing the manual effort of applying formal methods in industrial practice. Our approach has been applied successfully on several industrial designs.