In today's SoC development, tremendous mask costs evince the need for first-pass silicon. The steep growth of verification complexity combined with shortened time to market requirements, necessitates the search for more efficient and automated verification practices.
The automation of Formal Verification (FV) is one possible solution to address the above problematic. 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.
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 high-level system properties are developed first since they tend to cover a group of features at once. 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 inputs of the Design Under Test (DUT) 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 was a corresponding request phase. When verifying an IP with an OCP slave interface (Figure 1), this property is used as an assertion (check) since the response phase is an output of the IP.
1. Verifying an IP with an OCP slave interface.
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 difficulty resides in the complexity of the OCP specification. The extreme OCP interface configurability enables the creation of a flexible system, but also increases a verification burden. Identifying the appropriate set of OCP properties might not be trivial, resulting in missed corner cases and verification holes.
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. To this point, the OCP-IP Functional Verification Work Group (FVWG) created an OCP-IP compliance plan. The compliance plan defines all OCP properties. 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 can be identified and proven. For a more complete description, please refer to the OCP-IP 2.2 specification, chapters 13, 14 and 15.
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 ) as shown in Figure 2.
2. Floorplan of core using OCP-based interconnects.
Click here for the complete floorplan
To minimize the verification effort of all these OCP interfaces, several EDA vendors decided to create an OCP VIP library. This library (on the left in Figure 3), contains all properties defined in the OCP compliance plan and is typically coded by one or more expert verification engineers in PSL/SVA + auxiliary VHDL/Verilog. The coding is a one 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.
3. Vendor supplied library interacts with the OCP verification environment.
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 problems (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's being applied to lots of 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 together with industrial clients.
Some OCP VIP experiences within TI
As shown in Figure 4, 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, )
4. Cadence's OCP protocol VIP integrates with TI designs.
Click here for a larger version
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, please 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 needed 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 will require 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 has a high chance to miss corner cases on the OCP interface 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 and the other one is used for the actual data flow, tend to be error prone and leave bugs when using pseudo-random based simulation approaches. Last but not least hard-to-find bugs as FSM dead-locks will have a higher chance to be found with formal verification then with pseudo-random simulation.
Overall we applied the OCP VIP methodology to several wireless OMAP projects with each around 50 IPs with 1 or more OCP interfaces. The bugs found range from hard-to-find corner cases up to architectural bugs.
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 (OCP, AXI, AHB). For internal protocols, a VIP can be developed (Power Management). By applying those VIPs (Figure 5) the verification engineer receives a 'free' environment as well as 'free' low-level protocol checks.
5. Protocol VIP can improve the verification environment.
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)
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.
About the Author:
Jeroen Vliegen is a Formal Verification Engineer at Texas Instruments WTBU (France).