Static Formal Verification for System Level Verification

Aniruddha Baljekar, Srinivas Puttur
NXP Semiconductors Pvt. Ltd.

Abstract :

Industrial data shows that verification takes about 70 to 80 % of the total project development time. With increasing complexity of the SoC, System Level Verification of the SoC is one of the key challenges to the verification teams. Improving TTM by reducing the Project Timelines i.e. by reducing the effort on System Level Verification without compromising on the quality of the deliverables is one of the challenges faced by the verification teams.

In this direction we have used static formal verification to complement the Metrix Driven Verification methodology in SoC verification. Static formal verification replaces some of the verification tasks normally done under dynamic simulation thereby reducing the regression re-runs to achieve coverage goals and to reduce the effort to write additional scenarios.

The scope of the paper is to explain “How to use Formal verification for System Level Verification” and how it complements CDV based methodology [2] for System Level Verification.

The paper captures following details:

Static Formal Verification for the following integration checks at SoC:

Interconnection checks
Arbitration checks in case of multiple masters
Bus, Bridges decoding, Address Map checks
Protocol compliance
Checking of the “X” values on the bus
Checking of the memory controller/memory (ROM/RAM) paths
IO mux checks
IO pad connections checks

Advantages of using Formal verification for System Level Verification

The environment uses following tools/vIP’s:

Incisive Formal Verifier (IFV) tool from Cadence [3]
PSL/SV based assertion libraries (vIP’s) for standard protocols (AHB, APB etc.)
PSL based assertion libraries for NXP specific protocols

1. Introduction

For our SoC verification we have selected the OVM methodology [1] due to the benefits like, scalability, coverage, constrained random generation etc it offers’. Since these take effort and the verification environment takes time to mature, we were looking at alternative ways to reduce debugging effort taken for SoC verification. In this regard we selected Static formal verification for the following integration checks at SoC:

Interconnection checks (reset, clock, interrupt connections, bus connections etc)
Arbitration checks in case of multiple masters
Bus, Bridges decoding, Address Map checks
Bus Protocol compliance
Checking of the “X” values on the bus (Multiple drivers on the bus)
IO mux checks
IO pad connections checks
Dead code checks
FSM related checks
Range overflow checks
Synthesis pragma checks

2. Motivation

Following are the motivation for looking at static formal verification to complement the standard CDV verification for SoC:

To reduce the overall system level verification time and reduce the debugging effort for the following:

Integration
Sub-module Integration
Protocol compliance at the interfaces of the various IP’s and bus peripherals

This is important as normally the integration of the SoC sub-systems and creating top level verification environment start at the same time of the project execution phase. The initial integration issues can be checked only when verification environment is available and basic interconnection tests are available. Till then it is not possible to check these aspects. The net result is that the debugging of the integrations related problems might take a longer time to identify and fix.

To reduce the debugging effort for the following:

Checking of the “X” values on the bus, uninitialized registers in the design.
Interrupt connections, bus interconnections, address mapping problems.

These problems can be easily caught during the verification phase using proven methodology like CDV. However if these issues are caught early in the integration phase when the verification environment is being created then it would help in reducing the verification time.

To reduce the effort for writing system level test cases for checking following:

o Checking system level address mapping
o Checking the decoding/arbitration of the various bus system of SoC
o Checking of the memory controller/memory (ROM/RAM) for proper memory address translation
o Interconnection tests
o IO mux checking
o IO pad connections
o To get a toggle coverage of at-least 99%
o Multiple bus drivers at any point, floating bus at any point in time, Bus contention at any point in time.

The setup time to put the verification environment for IFV checks is minimum and fast.
Debugging of the failing assertions is quite easy as tool displays the required set of signals related to an assertion automatically. Hence time taken to locate the bug is drastically reduced and verification engineer can find out the conditions for assertion failure and hence locate the bug.

Figure 1 Debugging assertion

3. Technical Details

3.1. Environment to check high speed bus-system

Figure 2 Environment to check High speed bus

Use the assertion library for the high speed bus protocol. (e.g. AHB, AXI etc)
Use the assertion library vIP master and vIP slave components in the environment
Use the ready assertion available as part of the assertion libraries to check for the protocol compliance of the bus-subsystem
Write additional assertions to check the address mapping of the bus decoder
In case of the multiple master bus-system the arbitration mechanism also can be tested
Use IFV to check the assertions for both the protocols compliance, address decoding at high speed bus, bus width etc.
The master, slaves are from the assertion libraries

3.2. Environment to check integration of high speed bus sub-system with peripheral sub-system

Figure 3 Environment to check bus 1, bus 2 with peripherals

Add the assertion libraries for the low speed bus protocol (e.g. APB, VPB etc) to the above environment with the assertion libraries for the high speed bus protocol (e.g. AHB, AXI etc)
Use the vIP assertion library master and slave components in the environment
Use the ready assertion available as part of the vIP assertion libraries to check for the protocol compliance of the bus-subsystem
Write additional assertions to check the address mapping of the bus decoder for the low speed bus
Use IFV to check the assertions for both the protocols compliance, address decoding at high speed bus and low speed bus, bus width etc.
The master, slaves in this case is from the assertion libraries (except for the bridge)

3.3. Environment to check integration of processor sub-system with peripheral subsystem with peripherals + IP’s

Figure 4 Full system with vIP master

Replace the all the slaves from the assertion libraries by the actual IP’s. e.g, Memory controllers, peripherals like uart, i2c, etc. Only master vIP is used to generate bus cycles.
Use the assertions from the above environment setup
Use IFV to check the assertions for both the protocols compliance, address decoding at high speed bus and low speed bus, bus width etc. with actual high speed IP’s and low speed IP’s

3.4. Environment to check IO pad and pin muxing + toggle coverage

It is very critical to make sure the Input-output pad connections are done correctly and all possible combinations are verified. Since under different register bit setting, same IO pin may get connected to different functionality, automation of this would greatly reduce the manual effort and give confidence on the IO pad and pin connections under various functional requirements of SoC. Figure 5 below shows a typical IO pad in a typical SoC.

Figure 5 Typical IO Pads in SoC

Figure 6 Automatic assertion generation using Excel sheet

IFV provides a way to automate the IO pad connectivity. These are the steps to be followed.

Enter the connectivity information in a excel sheet as show in Figure 6.
Export the excel sheet into a .csv file.
Use the utility provided by the IFV to convert the information present in the .csv file to a set of assertions in a vunit.psl file. This vunit.psl file is used with IFV to check the IO pad connections.

4. What the verification approach offers? The verification approach offers/enables following:

Reduced effort towards interconnection, address decoding, memory aperture checks, system memory map checks. The out of the box assertions available as part of the assertion libraries enables checking of the protocol compliance of the subsystems. Besides setting of the environment to do these checks is minimal and its possible to check the integrated sub-systems for all possible bursts types supported by the bus which may-not be possible in the scenario when the actual IP supports only sub-sets of the burst types. The effort required to put the environment together typically is about 2-3 days. The major effort is only towards the debugging of the IP’s incase of non-compliance of the protocol by the IP. Very little time is required to write additional assertions for checking decoding/address mapping specified for the SoC.
Incorrect connection, multiple drivers, address width mismatch is easily caught in this approach.
Found peripheral address map overlap due to different address widths required by Bus-1 and Bus-2.
Detected APB low power compliance issues
Detected the problem with pready generation by a APB slave.
Corner test cases which may not be possible to check with SoC level tests in simulation can be easily checked in this approach

Generation of deadlock condition between peripherals and cpu.

Pin muxing and IO pad connections can be checked in this approach
Toggle coverage can be checked by adding specific assertions. Effort to write additional test cases to get the required toggle coverage at simulation can be avoided.
The functional coverage can be turned on using assertion base vIP’s. E.g.: AHB protocol coverage information can be generated with +coverage option.
This approach can be taken in parallel without any dependency on the SoC environment design/availability. However its not a replacement of the simulation based regression test cases.
The auto checks offered by IFV gives good insight into the RTL in-terms of detecting dead code which would have taken few regression runs with total random stimulus, analysis of code coverage and then few iterations of directed tests to identify and analyze the presence of dead code.
Ease of debugging as it pin points the location of failure as well as displays the relevant signals to trace the cause of the problem.

5. Next Steps

To reuse the IFV related files in a different product and measure the verification effort reduction.
Creation of generic library to be re-used across IP, sub-system and System level verification and share it across different business units.
Re-use of the assertions written during dynamic simulation.

6. Summary

As explained in this paper, we have been able to set up the verification environment using IFV in parallel to the verification environment developed using CVD with OVM methodology. We were able to identify around 6 bugs in the area of interconnections in very less amount of time and were able to save about three weeks effort on dynamic simulation, debugging and regressions. Going forward we plan to re-use the IFV setup and our learning with IFV in future product and are confident that we can reduce our verification effort for dynamic simulation by even larger extent.

7. Limitations

There are very few assertion based vIP’s available from cadence. In case Processors like MIPS, ARC are used, protocol compliance assertions needs to be coded or you need to buy vIP from third party vendors.

8. References

[1] OVM reference manual from OVM world (www.ovmworld.org)
[2] IPCM documentation from Cadence
[3] IFV documentation from Cadence

Abbreviations: