Dynamic Assertion Based Verification using PSL and OVL

Aniruddha Baljekar, Philips Semiconductors
Bangalore, INDIA
    
Abstract:

Verification is one of the most critical and challenging tasks, which takes almost 50 % of the complete design and verification cycle. With the complexity of the designs on the rise and with that also the verification effort, new challenges are to reduce the life cycle by adapting new methodologies which help the existing development and validation methodologies, used by the design teams.

Assertion Based Verification is such a methodology, that augments the existing design and verification flows used in the development of an Intellectual Property and cuts down the verification and validation cycle.

The scope of the work with dynamic assertions was to implement property checking using dynamic verification tool like Cadence IUS, using assertion language like PSL and OVL library in a RTL. The work resulted in application notes intended to aid design engineers to easily adapt this methodology and give a jump-start in using assertions. It also gives suggestions on:

• How to add assertions in PSL or OVL in a design
• How to add assertions in an existing or legacy IP
• How to add assertions in an new IP
• Mentions about the assertions overhead on simulations

Further to this, deployment of the methodology within the design group will give the measure of the actual benefits in using assertions. Follow up activities to this work on dynamic assertions is to deploy on a design within a design group and static assertions using static property checking tools.

The session captures the essence of the methodology, how to write dynamic assertions using PSL, OVL and the various ways of writing assertions (for new design and legacy designs etc.) and the terminologies used in ABV using PSL. It also dwells upon library-based approach to create re-usable verification components.

It also describes the IP for which assertions were written as part of the experimentation with the methodology, which has resulted in the recommendations towards implementation of assertions.

1. Introduction:

Motivations for this exercise

Verification takes about 50% of the project time. With the complexities in the design components on the rise, functional verification and coverage of the design is one of the challenges to the design and verification team. Reducing the verification time without compromising on the quality of verification is “the challenge” to the design and verification teams’ et-al.

Rationale in looking at ABV methodology

ABV augments the existing verification strategy adopted by the design teams without major changes in the verification strategy adapted by the design team. The Properties, which capture the specifications of the DUT in an executable form, are verified throughout the development and verification phases. Properties are written keeping the specifications of the DUT in mind and not how it’s implemented. It is reusable for both dynamic and static verifications.

Approach taken to have a better understanding of the methodology

ABV being relatively a new methodology with limited usage within the design teams, our focus was first on dynamic ABV dynamic (HDL simulation) using simulators like Cadence IUS.

PSL and OVL assertion libraries were considered to cover the DUT specifications in assertions. There were many reasons for this. Few of them were that it should be vendor independent and it should be relatively easy for the design or the verification teams to adapt.

Select an IP as a DUT and cover the functional specifications of the DUT under assertions using PSL and OVL.

Write an application note on the ABV methodology, which would give a jump-start to the designers on adapting this methodology. The intent of the document is to complement the existing documentation available on PSL and OVL from Accellera and Cadence.

2.  Details:

DUT is a Generic Interrupt Controller IP from Philips. The test environment uses Specman Elite (for test vector generation and scoreboard checks using AHB eVC), Cadence IUS for dynamic simulation.


Overview of testbench setup

The specifications of the DUT are captured in assertions using PSL and OVL respectively. The PSL assertions can be enabled or disabled during simulation (using the “–assert” pre-compilation flag with Cadence IUS during compilation) while the OVL assertions are enabled or disabled using a global flag.

Constraints

Design is a legacy IP. Given this situation and developers of IP being a different, the assertions had to be put outside the design and could not be embedded in the design.

Approach

• Identified the specifications/requirements of the design to be covered under PSL and OVL assertions
• Writing assertions in the top-level of the design
• Internal signals of the DUT used in the properties and covered under assertions had to brought out to the top-level using the “nc_mirror” utility provided by Cadence IUS
• Added assertions using OVL libraries in the top-level module
• Added assertions using PSL in a separate file using “vunit”
• Identifying the test scenarios and test cases to check the functionality of the DUT

Note: AHB protocol checking is performed by the AHB eVC. Assertions check the functional specification of the DUT

3. Results:

Capturing the practical experimentation in an Application note. The application note typically covers details, which is intended to help the verification engineer in adapting the methodology and in the implementation of assertions.

Application notes cover following:

• Recommendations on the typical design components that can covered under assertions
• Protocols
• FSM
• Stack
• FIFO
• Memory
• MUX
• Datapath
• Checks for illegal values
• Checks for “X” and “Z” values
• Exceptions and corner cases
• … etc.
• Recommendation on adding assertions to an existing design
• Recommendation on adding assertions to a new design
• Recommendations on property/assertion coding
• Property naming guidelines
• Mechanism to enable and disable the assertions and its associated auxiliary code during compilation
• User specific error reporting mechanism
• Placement of properties and assertions within the code (embedded in the code) and outside the code
• Auxiliary code for capturing the specifications of the DUT to have implement simpler and user comprehendible (self explanatory) assertions
• Create libraries for commonly used properties/assertions. These libraries can be used seamlessly across the design groups
• Use auxiliary code in implementation of assertions. It helps in debugging the failure of the assertions using these internal signals.
• Guidelines and interoperability for writing assertions
• To improve simulation performance
• Write simple assertions. These run faster and debugging also is easier.
• Use clocked assertions for synchronous behaviours. Use unclocked assertions for asynchronous models.
• Avoid unnecessary overlapping behaviour and enables
• Add abort conditions to the assertions if required to avoid failures during such sequences e.g. reset condition
• Use strong properties for the assertions that are required to finish during the simulation

Benefits in using ABV

• Improves observability of the design

• Using assertions one can create unlimited number of observation points anywhere in the design
• Enables internal state, datapath and error pre-conditions coverage analysis

• Improves debugging of the design
  

• Assertions help capture the improper functionality of the DUT at or near the source of the problem thereby reducing the debug time.
• With failure of the assertions one can debug by considering only dependent signals or auxiliary code associated to the specific assertion in question
• Assertions also help to capture the bugs, which do not propagate to the output.

• Improves the documentation of the design
• Assertions capture the specification of the design. I.e. the specifications of design are translated into an executable form in the form of assertions, assumptions, constraints, restrictions. The specifications are checked during the entire development and validation phase.
• Assumptions capturing the design assumptions continuously verify whether the assumptions hold true.
• Assertions always capture the specifications in a concise form which is not ambiguous i.e. assertions are the testable form of requirements
• Assertions go along with the design and can also be enabled at SoC level.

4.  Conclusions

PSL vis-à-vis OVL

• o    PSL is more powerful than OVL
• PSL is an assertion language unlike OVL. (OVL are libraries of pre-defined simulation monitors in VHDL/Verilog)
• PSL is vendor independent and is supported by a wide vendor base
• OVL lacks expressiveness to specify a property concisely
• Assertions implemented using PSL are self-explanatory
• OVL does not provide coverage details at the end of simulation. With PSL one can check out the properties that have not been hit during simulation, which enables the verification engineer to enhance his testbench to cover the assertions which were not activated during simulation
• Description of the properties using PSL is more concise and readable compared to OVL modules. One should know the functionality implemented by the OVL module used to specify the specification of the DUT to understand the intent of the assertions. In case of PSL this is more readable and can be easily understood by others, who were involved in the writing of the assertions
• Lots of auxiliary code needs to be added to check the specification using the modules available with OVL
• With OVL the assertions necessarily need to be embedded in the design. With PSL the assertions can be embedded in the design or can be included in a separate file using “vuint”
• OVL libraries are available as VHDL, Verilog modules. PSL assertions supports VHDL, Verilog and SystemC
• o    Advantages of OVL
• Its an Accellera standard
• Vendor independent
• Library of pre-defined simulation monitors
• Source code available in VHDL and Verilog
• User specific error messaging supported
• User can specify the severity level for the assertions
• Ease of use as the designers are conversant with VHDL and Verilog
• o    Assertions overhead on Simulations
• This is dependent on the density of the assertions added to the design. However in the present case, with Interrupt controller as the DUT and with assertions (20 PSL assertions and 20 OVL assertions) the overhead on simulation was about 1%. This needs to be further analysed with a bigger design (with more density of assertions) at Unit level and at SoC level

5. Way Forward

• Deployment of ABV methodology with the Business Lines or Business Units (IP development teams). This would result in easy adaptability of the methodology by the design teams and measure the practical benefits from this methodology [Verification time saved etc.].

• Measure the simulation overheads due to assertions at Unit Level and SoC level.

• Extend the ABV methodology to include writing assertions for SystemC designs.

• Extend the ABV methodology to include static verification using formal static verification tools like Cadence IFV

• Include comparisons in writing assertions with assertion languages like PSL, “e” etc.

6.    Acknowledgements and References

	Title	Author
[I]	Property Specification Language: Reference Manual (Version 1.1)	Accellera
[II]	Open Verification Library Assertion Monitor Reference Manual	Accellera
[III]	Assertion Based Design From Kluwer Academic Publishers	Harry Foster, Adam Krolnik, David Lacey
[IV]	Simulation-Based Assertion Checking Tutorial	Cadence
[V]	Simulation-Based Assertion Checking Guide	Cadence
[VI]	Datasheet Philips Generic Interrupt Controller IP

Acronyms:

ABV	Assertion Based Verification
PSL	Property Specification Language
DUT	Device Under Test
“e” Language	Verification Language of Specman Elite
HDL	Hardware Description Language (VHDL or Verilog)
IP	Intellectual Property
OVL	Open Verification Library from Accellera. Its an open library of assertion components
RTL	Register Transfer Level
Specman Elite	A Functional Verification tool from Cadence

Definitions:

Property	A collection of logical and temporal relationship between Boolean and sequential expression that represent a set of behaviour. Properties are associated with the design under test (DUT)
Assertions	Assertions are properties of/or about the design that are supposed to be true
Constraints	Constraints are properties about the interfaces of the design
Assumptions	Assumptions are constraints. Assumptions are statements of the about the interface to the design that are supposed to the true
Restrictions	Restrictions are constraints which express the behaviour that is not true about the interface to the design
Boolean layer	A property’s Boolean layer is comprised of Boolean expressions composed of signals within the DUT.
Temporal layer	A property’s Temporal layer allows to describe the relationship between the Boolean expressions with each other with respect to time
Verification layer	Verification layer specifies how a property would be used. i.e. if whether property should “assert” or “assume” or “restrict” or “cover” is described by this layer. In dynamic simulation “assert”, “assume” and “restrict” are treated as “assert”. These are interpreted accordingly by formal tools
Assert	PSL directive “assert” states that the property is treated as an assertion during verification
Cover	PSL directive “cover” states that the property is treated as a functional coverage point
Assume	PSL directive “assume” states that the property is an assumption for the design. Its treated as an assertion in dynamic simulation
Restrict	PSL directive “restrict” states that the property is a restriction for the design. Its treated as an assertion in dynamic simulation