Abstract

Verification is one of the most important and difficult part of System-on-chip (SoC) design. In the electronic industry today, the combination of increasing complexity of today’s ASIC designs and relentless time-to-market pressure have resulted in big challenges to verification, especially functional verification. The need of automatic verification and IP reuse solution became more and more urgent.

The objective of this paper is to share the effective method of using Synopsys’ hybrid-formal verification tool Magellan and reusable assertion IP (AIP) to verify your designs. In our project of OCP2AHB bridge verification, we build our testbench by connecting OCP AIP and AHB AIP to double sides of the bridge directly. The high-coverage stimulus is generated with Magellan to test all the properties and assertions of our testbench. It is proved that this verification method can easily build a testbench and verify the function of our design completely.

Key words: Magellan, AIP, function verification, IP reuse, hybrid-formal verification

1. Introduction

Nowadays, the scale of SOC design is greatly larger than before, and the integration becomes more and more complex. This increases the probability of making mistakes in circuit logic and function design. To guarantee the function correctness, verification takes an important part during whole chip design flow. In fact, for many teams, verification takes 50%-80% of the overall design effort. How to improve our verification methodology and how to shorten the period of verification has become the target of verification engineers to making effort to. The objective of this paper is to attempt a new verification flow using assertion and hybrid-formal verification technology to complete our verification work.

In the verification of complex designs, engineers should write as many test files as possible to test various functions of the design modules. Even though, some corner case may easily be missed. In this aspect, hybrid-verification tool present its advantages, it makes use of static formal mathematical techniques and dynamic random simulation to generate random stimulus with constraints and test properties or assertions that are important to the correct operation of your design. Then it automatic displays the results of simulation and the potential bug of your designs.

In this paper, we use VCS reusable bus assertion IP (AIP) to build an OCP2AHB bridge testbench. And use Synopsys hybrid-verification tool Magellan to work on function verification. The results of this verification have met our expectation, and complete the module verification in a short time.

The following of this paper will expatiate on the hybrid-formal verification flow, the usage of AIP and the framework of our OCP2AHB bridge testbench. The results of this verification will be analyzed at the end of this paper, and the conclusion will be given.

2. Magellan verification flow

Figure 1 shows the Magellan verification flow.

To run Magellan, firstly, analyze the design specification and abstract all the functions of your design. Taking care of two points: what constraints should be added for input signals, and what function should be checked of the design module. Then describe these input constrains and function checkers with assertion language. In our verification, we use SVA to take this job.Secondly, create a Magellan project file that is composed of TCL commands. Add the RTL design files. Add an environment module that defines simulation options, clock and reset signals, and any other supporting files for the DUT. Add a session module that includes input constraint files, assertion checker files and coverage collection files.

Lastly, run the project in Magellan. Magellan will attempt to prove all the properties by mathematically analyzing the design. After the running complete, it will present all the property violations and generates a sequence of stimulus vectors for debug.

3. VCS assertion verification model AIP

To verify our OCP2AHB Bridge with Magellan, we build an assertion based testbench with VCS OCP AIP and AHB AIP. They greatly save our time on testbench developing. These AIPs include bus protocol assertion checkers and coverage collection. We just bind these AIP with our design and pass valid values to the configuration parameters to enable the corresponding function checker based on our design requirements.

3.1 OCP AIP

The VCS OCP Assertion IP has independent checker modules for OCP Master-Slave and System-Core interfaces for protocol compliance. This provides a convenient way to verify the protocol correctness of OCP interfaces in a design. Our OCP2AHB Bridge designs compliant with OCP Master-Slave protocol. In OCP AIP the corresponding check module is SnpsOcpMasterSlaveChecker.

The SnpsOcpMasterSlaveChecker has properties of OCP master and OCP slave. We should turn on both MASTER_ENABLE and SLAVE_ENABLE parameter to make these properties active. In our testbench, The OCP2AHB Bridge is regarded as an OCP slave. So we use OCP master properties to constrain the OCP bus input, and use OCP slave properties as checkers to prove the DUT function. Additionally, the AIP can be enabled to track functional coverage if you turn on the parameter COVERAGE_ENABLE.

Figure 2 shows a simple testbench which uses VCS OCP AIP to test an OCP slave.

Figure 2: OCP slave testbench with OCP AIP

3.2 AHB AIP

The VCS AHB AIP can be used to verify any AMBA AHB Master, Slave, Arbiter, Decoder interface. For our design, the OCP2AHB Bridge is treated as an AHB master. So we use AHB master check module SnpsAhbMasterChecker in AHB AIP to verify the function of AHB bus. This SnpsAhbMasterChecker has its own constraint properties and checker properties for AHB master. We can just use the parameter CONSTRAINTS_EN and PROPERTIES_EN to control these properties. Optionally the AIP can also be enabled to track functional coverage by turning parameter COVERAGE_EN on.

Figure 3 shows a simple testbench which uses Synopsys OCP AIP to test an AHB master.

4. OCP2AHB bridge testbench

Feature 4 shows the testbench framework of OCP2AHB Bridge.

Figure 4: OCP2AHB testbench framework

It is made up of OCP AIP, AHB AIP, additional constrains module, and bind files. The additional constraints are created to comply with the special needs of our design input signals. The bind files bind the AIP and other property modules with our design by mapping the design module port with those of the assertion module. The valid values pass to the configuration parameters of the AIP are also process in these files.

4.1Create project

To run in Magellan, We first create a project file OCP2AHB.prj with TCL commands in the recommended order and add the design files to it. This project includes an environment module (e0), 5 property modules (p0, p1, p2, p3, p4), and a session module (s0).

The environment module e0 includes a reset model, a clock generator model and some other input signal control model. The reset model point out which signal is the reset signal, what level state is the effective reset state, and the length of reset phase. We use command add_env_port –name –reset and set_env_reset –defaultLen to specify them. The clock generator model is created according to the design requirement. For our design, there are three clock sources, cpu_clk, hclk, and hclk_phase. Feature 5 shows the phase relationships of these three clocks. We use command add_env_port –name -clock –waveform to specify clock period and phase. The input constraint model is for the special need of some input signals that should be driven to non-zero value during reset, and some signals that should hold on to a constant value after reset. We specify them using command add_env_port –name –reset and add_env_port –name –constant.

Figure 5: the clock relationship

We just take 2:1 clock ration as an example, the following figure 6 is part of our environment module.

4.2 Input constraints property

For the input signals, the constraints in environment module are not enough. Magellan applies random values to input signals at the subsequent clock cycle after reset phase. In real application, we need random input to cover all the possible cases, but this random value should be compliant with some bus protocol to ensure that Magellan applies legal stimulus to the design.

To make our OCP2AHB bridge input signals complaint with OCP and AHB bus protocol, we add the OCP AIP master property p0 as constraints to OCP bus input signals and AHB AIP slave properties p3 as constraints to AHB bus input signal. Additionally, there are some extra constraints p4 created to meet the special need of our design.

In the project file, we use define_property –constraint command to define the attribute of these properties as input constraint. Use command add_property_info –scope include all the properties that you need to testbench. Figure 7 shows the constraint in OCP2AHB bridge testbench.

Figure 7: Constraint module

4.3 Function checker property

To verify the functions of OCP2AHB Bridge on both sides, we add OCP AIP slave property to property module P1 as OCP bus checkers, and add AHB AIP master property to property module P2 as AHB bus checkers.

Feature 8 shows the commands that create function checker module. Command define_porperty –checker is to tell Magellan treat the property as checker. Command add_property_info –scope include the property of AIP that meet our design requirement, and option –exclude is to turn off the property that we don’t need.

Figure 8: Function checker module

5. Verification result

After running in Magellan, use a list_session_results –summary command to see the summary compile information. Magellan generates a report that shows the status of each property (proven, falsified, or unknown).The following report is the results of our OCP2AHB bridge design running.

Magellan has found 21 properties for property module p1 and 15 properties for property module p2, 17 properties in p1 and 8 properties in p2 have been proved, 12 properties are unknown state. There are no falsified properties of our design.

Magellan provides GUI (mgui) to develop, run, and monitor test results. This is an easy-to-use way to debug our design with graphic interface. When there is a property which is falsified, Magellan will generate a corresponding stimulus to present the false property. Figure 9 is the waveform that Magellan generates to show the violation of property.

This SnpsAhbErrmLockBurst_check is a checker property in VCS AHB AIP. The waveform indicates that AHB master has disserted HLOCK in the middle of a non incremental burst at 1320ns and 1400ns.

It is effective and convenient to fix the position of the bug with Magellan. If the bug violate your design require, you can just modify your RTL design and redo the Magellan compile until it meet the goals. If this is the special need of your design, you can just turn off this property in the project file.

6. Conclusion

It is a new attempt for us to using VCS AIP building testbench and using hybrid-formal verification tool Magellan debugging our design module. Using this verification flow has reduced our verification period and improved our verification quality. It has proved that this is an effective and convenient way to locate the bugs of the design, especially, the corner bugs. With combination of Magellan and dynamic verification, the verification work will be easier and sufficient.

7. References

[1] Magellan User Guide (Version MG_2006.06-SP2), Synopsys, July 2007.

[2] AHB Assertion IP User Guide (AHB_AIP_2008.06-1.lca), Synopsys July 7, 2008.

[3] OCP Assertion IP User Guide (OCP_AIP_2008.06-4.lca), Synopsys, 7th July, 2008.