Automated Formal Verification of OCP based IPs using Cadence's OCP VIP library

1 Introduction

In today’s SoC development, high mask costs exacerbate the need for first-pass silicon. The steep growth of verification complexity combined with shortened time to market requirements, necessitates a search for more efficient and automated verification practices.

The automation of Formal Verification (FV) is one possible solution to address the above problems. Complementary to well-established pseudo-random verification techniques, FV enables the verification engineer (or the designer) to exhaustively prove specific parts of a circuit. This paper discusses the automation of FV for bus protocols like OCP.

2 Property concept

To formally verify any IP, the designer / verification engineers must extract a list of properties from the specification. Each property describes one or more features of the IP. Preferably highlevel system properties are developed first since they tend to collectively cover a group of features. Low-level properties approach the RTL and therefore generally prove less functionality.

Each property can be used by a Formal Verification tool (such as Cadence’s Incisive Formal Verifier) as an assertion (check) or an assumption (environment constraint). Most of the time, assumptions are applied to the DUT’s inputs and assertions to the DUT’s outputs. In the OCP protocol for example, there exists a property which states that a response phase can only start after there is a corresponding request phase. When verifying an IP with an OCP slave interface (see figure below), this property is used as an assertion (check), since the response phase is an output of the IP.

3 OCP protocol FV

When verifying an IP with one or more OCP interfaces, theoretically, one simply has to extract the OCP properties and formally prove them. Practically speaking, this is not the case. The main challenge resides in supporting the complexity of the OCP specification. The great configurability of the OCP interface enables the creation of a flexible system, but also increases a verification burden. Identifying the appropriate set of OCP properties might not always be trivial, so missed corner cases and verification holes must be avoided.

It’s clear that a complete list of OCP properties for all possible OCP configurations is required. This need was identified early-on within the OCP-IP organization. For this reason, the OCP-IP Functional Verification Work Group (FVWG) has created an OCP-IP compliance plan. The compliance plan clearly defines all OCP properties in English. It also outlines, for each property, which configuration parameters activate the property. As such, based on the OCP interface configuration, only the relevant subset of properties need to be identified and proven. For a more complete description, please refer to the OCP-IP 2.2 specification, chapters 13, 14 and 15.

4 The OCP VIP library

Many of today’s high-performance SoCs (like Texas Instrument’s OMAP multimedia application processors for example) are OCP-based. Several masters or master-subsystems are linked through OCP-based interconnects with various slaves (peripherals, memories, etc …).

To minimize the verification effort of all these OCP interfaces, a group of EDA vendors decided to create an OCP VIP library. This library (on the left in the figure below), contains all properties defined in the OCP compliance plan and is typically coded by 1 or more expert verification engineers in PSL/SVA + auxiliary VHDL/Verilog. The coding is a 1 time effort.

To select the appropriate sub-set of properties for a specific OCP interface, a script parses the OCP configuration file (also referred to as the IP_rtl.conf). The final set of properties can be used by the formal tool as either assertions or assumptions.

The library will also contain a large set of covers. Covers are extremely important since they will detect an over-constrained environment. They will also enable the detection of false-positives (assertions in which the enabling condition is not reacheable). Vacuity errors can therefore be avoided.

Last, do not underestimate the development of a robust protocol VIP. Apart from the fact that the properties are well-defined by OCP-IP, there can be plenty of implementation challenges (errors in the PSL, auxiliary Verilog or even the property sub-set selection parser). This points directly to the fact that the library must undergo a solid testing phase in which it is applied to many IPs with different configurations. Large EDA vendors are usually well-positioned to carry out this task since they tend to have a vast internal IP regression database. To complete the testing phase, exhaustive testing usually is performed in collaboration with industrial clients.

5 Some OCP VIP experiences within TI

Within the Wireless Terminals Business Unit (WTBU) of Texas Instruments France, we easily integrated the Cadence OCP protocol VIP into our internal design flow. As can be seen in the figure below, the only (template) files we had to define were the:

• .f : which drives IFV
• .tcl : which initializes the circuit
• .psl : which models the non-OCP primary inputs (resets, test, power management, …)

The user simply has to:

• call a Makefile target to analyze and elaborate the RTL
• call a Makefile target to parse the IP_rtl.conf and obtain the property sub-set
• edit the template files (.f/.tcl/.psl)
• and finally … run the formal prove with IFV to prove OCP compliance

To give an idea of the simplicity & efficiency of the verification flow, consider the following. An engineer verifying an IP with a basic slave OCP interface takes, on average, between 30 minutes and 1 hour to exhaustively verify the OCP interface. The majority of time spent, is the time to edit the template PSL files for the primary input constraints. Note that this is a 100% exhaustive verification result. A more traditional pseudo-random simulation environment requires the instantiation of an OCP eVC, the writing of a random test case and most importantly a solid definition of the functional coverage. The dynamic regression may miss corner a corner case due to gaps in the functional coverage definition. The typical corner case which we found to be missed by dynamic simulation in many modules, is the OCP interface behavior when the IP is undergoing a software reset while some OCP transfer(s) is (are) still outstanding. Also, blocks with multiple OCP interfaces in which one is used to configure the module while another is used for the actual data flow, tend to be error prone and leave bugs when using pseudo-random-based simulation approaches.

Overall we applied the OCP VIP methodology to several wireless OMAP projects with each containing around 50 IPs with 1 or more OCP interfaces. The bugs found range from hard-to-find corner cases up to architectural bugs.

6 Using protocol VIPs for FV of higher-level features

An IP typically has: a clk & rst interface, a Power Management (PM) interface, an interface to configure its internal registers and 1 or more functional busses to communicate with the outside world (serial protocols, memory, …).

For standard protocols which are commonly used in a SoC, a protocol VIP is very likely to exist . For internal protocols, a VIP can be developed (Power Management). By applying those VIPs (see figure below) the verification engineer receives a ‘free’ environment as well as ‘free’ lowlevel protocol checks.

Based on this, the engineer can write higher–level system properties. Best-case, the system level properties can be proven without even having to model the missing interfaces (func1 & func2). In this case, the prove is more abstract since is was performed in an under-constrained environment. If counter-examples however show valid violations, the remaining interfaces have to be modeled.

Some examples of the most common high-level properties we developed are:

• Packet conversions through a bridge
• Memory & cache coherence
• Performance & latency properties
• Data integrity (is less suited for formal but still worth a try)

7 Conclusion

The automation of formal protocol verification using VIPs enables a rapid and exhaustive verification of critical IP interfaces. Once a VIP library is written and tested, it can be re-used to improve the verification quality and shorten the verification schedule. Last VIPs can also be used to ease the verification of high-level system properties since they provide a ‘free’ environment.