Introduction
The Open Core Protocol (OCP) is a synchronous socket interface specification that is widely used in the semiconductor industry today for System-on-Chip (SoC) designs. The flexible nature of the implementation makes it widely applicable to many different hardware applications that require a simple, robust data transfer protocol. The OCP International Partnership, a group that is dedicated to proliferating the OCP standard, estimates that OCP has been used in numerous SoC designs which have already shipped in many hundreds of millions of units. The popularity of this protocol is increasing rapidly as more designers become aware of the benefits of a flexible standard.
Naturally, along with the advantages of flexibility come many variants of the implementation that fall under the official protocol specification. While this makes it easy to adapt the protocol to the individual requirements of a specific design implementation, it does present a challenge for the verification team. Verifying protocol interfaces is a challenging exercise for any verification group. Formal verification of protocols has become far more prevalent in recent years because of its ability to exhaustively remove all doubt of incorrect interface behavior prior to tape-out. This article presents a basic overview of OCP covering both the basic operation and configuration files. It then introduces a configurable OCP formal verification IP generator that automatically creates appropriate OCP properties for a specific to design implementation of the protocol. These concepts are used to demonstrate a silicon-tested method of developing a verification plan for OCP designs.
OCP Overview
OCP uses a simple master/slave configuration. All signals are synchronized on the rising-edge clock. It uses a very simple read/write command structure to pass information between components. It supports both blocking and non-blocking forms, along with basic pipelined operations. The specification is completely bus-independent, with device selection and arbitration performed outside the OCP logic. Figure 1 shows a basic OCP representation.

1. This implementation is a basic example of OCP.
Multiple read and write commands make up the basic command structure of the protocol. Read (non-blocking), ReadLinked (blocking), and ReadExclusive (blocking) are some of the more common read commands. The write command also contains several forms, including Write (non-blocking), WriteNonPost (blocking), WriteConditional (blocking), and Broadcast (linked multi-device). OCP signals are divided into three main groups: dataflow, sideband, and test. Basic operation requires only a small subset of the dataflow signals. The sideband and test signals are optional in this configuration.
Because of the many possible configurations for OCP, the specification requires the protocol interface to be defined within a text-based configuration file. This file identifies the design-specific parameters such as data command subsets and modes, data and address widths, burst sequence and alignment, data handshaking, and optional signals. The parameters can be explicitly declared in the file or loaded from default settings. Figure 2 shows a sample configuration file.

2. The OCP configuration file is reasonably straightforward.
The Challenges of OCP Verification
The configuration file provides great flexibility for customizing the OCP details for a specific architecture. In its simplest form, OCP contains only two signals, while the complete specification contains greater than 50. Such variety in the protocol interface creates flexibility for integration, but with that flexibility comes challenges for verification, particularly when considering verification IP reuse goals.
The OCP specification does contain standard property sets for protocol compliance, and several vendors have created pre-packaged property sets based upon this description. Unfortunately, many of the properties in the specification are simulation-centric by design and are not modeled appropriately for other verification technologies such as formal analysis. Formal verification provides the highest confidence level in verification today, and protocol verification is an ideal application to benefit from its strengths. Verification teams with access to formal-friendly OCP verification kits not only reduce their verification cycle time, but also increase their confidence in the design behavior over running simulation alone.
Most pre-packaged OCP verification kits exhibit another problem beyond formal compatibility. The high degree of configuration freedom in the protocol makes it necessary for engineers to determine which properties in the verification sets are meaningful for the design and which can be safely ignored. If this effort is not performed up front, a significant portion of the properties might fail during verification. Debugging these properties on a live design can result in significant verification cycles spent simply trying to determine whether a given failure is reasonable. Understanding what can be safely ignored requires knowledge of what parts of the protocol checking are not required for the particular design under test. The time saved by using a pre-packaged set of OCP checkers can easily be lost or exceeded in the resulting debugging effort if the property set is not well matched to the level of OCP implementation. Engineers who have had to endure this process in the past often consider this to be one of the most difficult issues in using pre-packaged kits. A better solution is needed.
|