Development and Formal Verification of On-Chip Protocol Converter

Abstract

Integration of multiple Intellectual Property (IP) s from different vendors and with user defined logic in a System-on-a-Chip (SoC) is possible with the existing sub-micron semiconductor technology today. Development of such a SoC will have several challenges like design complexity, verification and timing closure.
Interconnection of various sub-systems and peripherals within a (SoC) design with a standard bus architecture has a number of advantages than distributed bus architectures. In a SoC, while interconnecting different IPs to a standard Fabric, there should be an interface between those two standard Fabrics. This thesis describes the work related to development of an On-Chip protocol converter, which is an interface between Intel Fabric and Advanced Extensible Interface (AXI) interconnect of Advanced Micro-controller Bus Architecture (AMBA).
Intel Proprietary protocol (IPP) is a bus protocol architecture which specifies the interconnection of Intel Fabric and its agents. Intel Proprietary protocol (IPP) follows Peripheral Component Interconnect (PCI) ordering rules, but External Interconnect architectures like AMBA AXI are not PCI compatible. To make IPP-AXI Bridge along with entire AXI Subsystem to participate in device enumeration, configuration and operation as a PCI device by the Operating system, a PCI configuration handler has developed. PCI Configuration handler will assist in PCI Power management and interrupt functionality for the On-Chip protocol converter (IPP-AXI Bridge). PCI Configuration handler is also assist in decoding the transactions initiated by other IPP agents to the AXI subsystem.
As this IPP-AXI Bridge has two standard interfaces. Deploying Formal verification ensures the interface specification valid for whatever the feature added to On-Chip protocol converter. Formal property verification environment has created to verify the On-Chip protocol converter with formal analysis. PCI Configuration handler has verified at block level using formal analysis before integrating it to IPP-AXI Bridge, which will used to resolve most of the bugs.
With the help of PCI Configuration handler, the IPP-AXI Bridge along with AXI subsystem is being enumerated as a PCI device logically, even though there is no true PCI hardware interface in the AXI subsystem. Formal analysis of IPP-AXI Bridge has resulted some bugs which are not discovered in normal simulation. Formal analysis at block level has improved the quality by exposing the basic bugs.