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.

OCP Verification
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 in its 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.

Essentials of Verification Planning

With a fully tailored set of formal-friendly OCP properties in hand, verification teams can begin the process of verifying that the protocol is implemented correctly within the design. In general, protocol verification often involves a large number of interrelated tasks, all of which must be accounted for before the design can be certified as compliant. Planning the necessary actions in advance helps coordinate the effort across multiple engineers to ensure the verification is completed on schedule. Planning also identifies prime formal analysis targets in the protocol early in the verification cycle. With a little up-front preparation, engineers can design a verification test plan that will leverage formal verification effectively alongside simulation where it can provide the greatest value to the overall verification effort.

Verification planning should address four fundamental questions in the verification flow:

• What is the design functionality that will be verified?
• How will each functionality be verified?
• What is the relative importance or priority of each feature to be verified?
• How will the team measure when the verification process is complete?

Answering these questions introduces predictability into the verification schedule, which is absolutely crucial in addressing time-to-market pressures. By understanding the key functionalities your team must verify, you can schedule the highest priority items first and assign necessary resources up front before they become scarce. Planning also gives engineering teams the option of determining which verification technologies and methodologies are appropriate for each verification task. It is here, in the planning process, that teams can select and prioritize formal verification targets. By taking time early in the verification process to plan out the tasks ahead, not only can verification teams ensure that no issue is overlooked, but they also set an accurate framework to evaluate the status of verification over time.

Planning software can aid verification planning. One such tool is Jasper Design Automation's GamePlan^TM Verification Planner. This tool provides a method for easily organizing design features you want to test, as well as powerful analysis and reporting capabilities.
This free tool uses a hierarchical plan structure. Hierarchical verification planning is an efficient way to ensure that all high-level issues are covered while still providing extensive coverage at the block or sub-block level. Planning begins with the natural-language statement of the intended behavior of the design under test. A reasonably detailed description of the behavior is essential to understand and communicate exactly what functionality you will test. The emphasis here is on what should be tested, not how it will be tested.

When verifying protocols such as OCP, the team should include the interface as one of the primary features to verify. Verification teams identify and document properties of each interfacing block to be checked. The protocol compliance checks contained within the OCP specification are a good source for these decisions. The team should also note any open issues identified upon examination of the connecting blocks to ensure they address them prior to completing verification. The team also prioritizes properties in terms of their critical nature to the project. This process quickly identifies key areas of focus throughout the verification flow and allows the team to assign appropriate resources. Figures 3 and 4 show examples of the early planning stages in a typical OCP interface design.

If the team members consider a particular set of functionality critical to the design's proper operation, they enter it on the list of potential candidates for formal verification. In many designs, it is important for the team to understand the characteristics of the blocks they will verify. While design components that are mainly data transformation, such as ALUs and DSPs, are generally not good candidates for formal in general, data transportation protocols usually are. Since OCP is primarily a data transportation protocol, we can apply formal verification across the design with few concerns for compatibility. Assuming the focus is on the interface components of the connecting logic, formal is a good technology choice for protocol verification, regardless of the data destination or source.

3. Verification Planning Starts with Describing Design Intent.

Click here for a larger version

4. Designers must weight the relative importance of property definition and resource assignments.

One caution to consider when choosing technologies for properties contained within the OCP specification is the form in which the spec describes the properties. For example, the OCP specification describes the following signal to have an unambiguous value during a request:

Most formal verification tools cannot process this property as described because they typically use synthesis models that expect two-value (0 and 1) logic representations for signals. In simulation, one can compare a signal against a value of "X" or "Z." In formal, such a comparison might not have any physical meaning, or it can vary depending upon what the vendor has implemented. If this check is considered a critical component for verification, you can often model it for formal verification, but in a different form. Often, appropriate logic to determine if data on a signal is valid already exists in the design, and the property can reference it for formal verification. In the worst case, the team can add such logic to the modeling layer of a PSL or SVA property description to maintain the state throughout analysis. It is important to note that none of these modeling methods require any changes to the RTL code itself. All permutations are contained completely within the verification code.

Once the functionality is defined, the focus changes to the strategies the team will use for verification. Critical functional areas of the design should use formal verification for the highest confidence in the logic. Teams can target other areas with a combination of formal analysis and simulation. At this point, teams determine coverage metrics, test cases, design constraints and assumptions about each of the features to be tested. Oftentimes, teams identify dependencies between properties at this stage. Documenting the dependencies helps ensure the robustness of the plan and completeness of the results. Where coverage holes exist, the team can schedule additional simulation or formal verification testing, as shown in Figure 5. Engineers perform analysis at this point to ensure the plan is complete and they have identified and documented all feature dependencies. With this plan in place, verification can proceed and a team can readily track it over the lifetime of the project. The plan is easily adaptable to changes in the design throughout the project lifetime by following this same process when introducing modifications.

5. Multiple verification technologies are used as shown in the coverage matrix.

Click here for a larger version

Summary

OCP is a flexible, synchronous, communications protocol in use in numerous designs today. 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.

References:
1) Open Core Specification v2.2 Rev 1.0, OCP-IP Association, 2007

About the Authors:
Jay Littlefield is Director of technical marketing at Jasper Design Automation. He holds an MS Degree in Electrical Engineering from Stanford University and an MBA from San Jose State University.
Øystein Kolsrud is an Application Engineer with Jasper Design Automation. He holds a MS Degree in Computer Science and Engineering from Chalmers University of Technology in Gothenburg.
Information about this article can be obtained from ocpinfo@jasper-da.com