OCP and Verification of Configurable OCP Interfaces

The Open Core Protocol (OCP) is a core-centric protocol that comprehensively describes the system level integration requirements of intellectual property (IP) cores. The flexible nature of the specification 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, confirms that OCP has been used in numerous SoC designs which have already shipped in many billions of units. The popularity of this protocol continues to increase 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 master and slave configuration. All signals are synchronized on the rising-edge clock. It uses a read and 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 illustrates a conceptual implementation of a simple system containing a wrapped bus and three IP core entities: one that is a system target, one that is a system initiator, and an entity that is both.

Figure 1. Wrapped Bus with OCP Instances

 

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.

              Figure 2. OCP Configuration File

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 that flexibility introduces 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 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 challenge 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.

Simplifying the OCP Verification Effort

In an ideal situation, a verification engineer has access to a property set relevant to the particular implementation of OCP in the design under test. A property generator creates a subset of the entire protocol automatically, based upon the design information. The setup is straightforward without requiring deep understanding of the protocol and requires few manual changes to the property set once completed. In this ideal situation, the resulting output is not restricted to a specific design or property language, and it is optimized for formal analysis. Jasper Design Automation provides such a capability via JasperGold’s OCP proof kit IP Generator.

The tool produces OCP property suites tailored for specific OCP configurations. Functionality outside a specific OCP configuration is not incorporated in the resulting output files. The IP Generator leverages the information within the OCP configuration file to tailor the generated properties to only those that are relevant to the specific design under test. Run times are nearly instantaneous, and the resulting output files are available in Verilog or VHDL flavors. The IP Generator supports property specification in either PSL or SystemVerilog Assertion (SVA) format. This support provides flexibility not only for use on internally developed OCP blocks, but also with purchased design IP configurations since you can generate equivalent property sets for mixed-code environments.

When using the IP Generator, engineers do not need to be experts in the overall OCP specification because the resulting property set is automatically minimized using existing design files. Moreover, the proof kit generates properties that are optimized for formal analysis, ensuring the most powerful tools for verification confidence are accessible without modifying simulation properties. You can automatically generate relevant OCP properties as interface constraints (instead of assertions to be verified) to ensure verification occurs under proper input requirements.

Users report reduced verification debugging time right from the outset because of the finely-tuned scope of the property sets. If the design specification changes over time, updating the verification environment is a simple matter of rerunning the IP Generator on the updated OCP configuration file. Subsequent design family generations with additional functionality no longer need to endure long debugging efforts to repeatedly identify and remove unused property sets. The IP Generator ensures that the verification environment includes only the properties necessary for verification of the specific design implementation.

Summary

OCP is a flexible, synchronous, communications protocol now shipping in excess of one billion units every year. The flexibility creates a great deal of opportunity to customize the protocol to only those specific functions required for a design, but flexibility in implementation generally means complications for verification. Designing a reusable verification environment presents challenges for the developers due to the highly customizable nature of the protocol.

If a team chooses to go with a pre-packaged solution, they must take care to ensure that the verification flow analyzes only the relevant portions of the property sets. This may require some level of protocol expertise to perform efficiently. If the team intends to use formal verification, they must take care to understand which properties are suitable and which they must rewrite. A better alternative is to leverage Jasper’s OCP IP Generator to automatically deduce the required subset of properties specific to the design. The flexibility of the output is readily adaptable to mixed-RTL designs and requires little additional OCP knowledge beyond what is already coded in the design. The OCP IP Generator produces output that is efficiently modeled for formal verification, providing the highest confidence levels possible for the verification environment.

Once the verification team identifies a formal-friendly OCP property solution, they can devise and execute a concrete verification plan. Protocol verification should be thorough, and OCP's configurability can create verification challenges if the team does not plan properly. By generating a hierarchical verification plan that clearly delineates the work to be done, the critical paths to be addressed, and the verification technologies employed, engineers can not only make their verification environments effective, but reusable. Verification planning tools can greatly ease the amount of work necessary to set up and maintain a verification testplan.

Alok Sanghavi is Technical Marketing Manager for Jasper Design Automation.  Prior to joining Jasper he was a Sr. Field Applications Engineer with Springsoft and Sonics Inc.  Previously, he was a Senior ASIC engineer with AMD and Interdigital Communications. He holds a BS in electrical engineering from Sardar Patel University in India, and a MS in electrical engineering from Polytechnic University, Brooklyn, New York. He is also currently pursuing an MBA from University of California at Davis.

Carlo Del Giglio is a Senior Field Applications engineer at Jasper Design Automation. He has more than 5 years of experience in formal verification. Prior to joining Jasper, he was a field applications engineer at OneSpin Solutions. Carlo holds a Master's degree in Electrical Engineering from the University of Ancona, Italy.

 

 

Alok Sanghavi is Technical Marketing Manager for Jasper Design Automation.  Prior to joining Jasper he was a Sr. Field Applications Engineer with Springsoft and Sonics Inc.  Previously, he was a Senior ASIC engineer with AMD and Interdigital Communications. He holds a BS in electrical engineering from Sardar Patel University in India, and a MS in electrical engineering from Polytechnic University, Brooklyn, New York. He is also currently pursuing an MBA from University of California at Davis.

Carlo Del Giglio is a Senior Field Applications engineer at Jasper Design Automation. He has more than 5 years of experience in formal verification. Prior to joining Jasper, he was a field applications engineer at OneSpin Solutions. Carlo holds a Master's degree in Electrical Engineering from the University of Ancona, Italy.

 


EECatalog Tech Videos

MAGAZINE

  • Download the latest issue of the Chip Design Magazine
    and subscribe to receive future issues and the email newsletter.

©2014 Extension Media. All Rights Reserved. PRIVACY POLICY | TERMS AND CONDITIONS