Archive for the 'Assertion Based Verification' Category

Srinivasan Venkataramanan, CVC Pvt. Ltd.

Abhishek Muchandikar, CAE, Verification Group, Synopsys

Raja Mahadevan, Sr. CAE, Verification Group, Synopsys

It is well understood and accepted fact that Assertions play a critical role in detecting a class of design errors (or bugs) in functional verification. Just like any other verification component in a robust, reusable environment, assertions need to be both controllable and observable from various levels including tests, regressions, command line etc. However an ad-hoc throw of assertions across the design and verification code doesn’t always consider this requirement upfront.

Recently standardized SystemVerilog 2009 construct checker..endchecker is definitely a good step towards creating a good encapsulation for these widely spread out assertions. In our recent book on SystemVerilog Assertions (2^nd edition of SVA handbook, www.systemverilog.us/sva_info.html ) we cover this construct in depth. We also presented a case study of a Cache controller verification using these new constructs at DVCon 2010 (paper & code available from www.cvcblr.com on request).

The role of a methodology goes far beyond the constructs, it does utilize them but provides more controllability and observability for the end user trying to make sense out of all these various features to achieve his/her final goal of getting verification done.

In this series of blog entries we try and cover some of the key aspects of such methodology role in adopting ABV (Assertion Based Verification). We welcome reader comments to add more innovative thoughts and ideas to this puzzle. Our goal of this blog series is not to cover all possible aspects of ABV methodology as that would include a wide range of topics, many of them already well covered in VMM book (www.vmm-sv.org); rather in this blog series we look at application aspects of ABV methodology.

To start with, let’s partition the role of methodology into two major buckets: observability & controllability.

Under observability we will explore the following:

· Make assertions observable in native form within the methodology framework

· Tie the assertion results to the verification plan via VMM Planner hooks

Under controllability we will explore the following:

· Control the severity & verbosity of assertions from external world – command line, testcases etc.

· Control assertion execution during reset, exceptions, low power etc.

Making assertions natively observable in VMM

In simulation based verification, observability is primarily enabled by the kind of messages that get emitted during the run. Messaging service plays an important part in a verification environment indicating the progress of the simulation or providing additional information to debug a design malfunction.  To ensure a consistent look and better organization of messages issued by various verification layers be it the transactor, scoreboards, or assertions, use of a standard messaging service is required. VMM provides a time-proven utility vmm_log to enable this key requirement. While the use of vmm_log in a typical VMM environment is well understood and widely deployed, the integration of the same to assertions is not that widely spoken about in the literature.

Assertion reporting as such always tends to be a loner in terms of the verification environment messaging family. This is due to the fact that assertion reporting has been handled in ad-hoc manner – many a times unattended (i.e. no action blocks at all), this can lead to simulator specific reports for assertion firings (pass/fail) where as the rest of testbench environment uses a consistent vmm_log style.

The drawback of such a use model is twofold:

· Absence of a single tightly integrated messaging service across the verification board

Assertion failures do not interact with the test bench environment and hence there is absolutely no way to effectively and correctly qualify the simulation. The limitation of such a behavior (in a regression setup), would never qualify the test as a “failures” unless some other post processing is duly placed

· Assertion results bear zero control over the verification simulation cycles

Quite often it is observed that the tests tend to run the entire simulation cycles even in the presence of assertions failures which maybe uncalled for and may warrant an immediate termination of the simulation.

Efficient incorporation of assertions in a verification environment calls for synchronization between assertion results and the verification environment. A common messaging service would be the key to such synchronization. The VMM messaging service “vmm_log” is a fine example of a standard messaging class which is seamlessly integrated into assertion checkers/properties which ensures consistency across the complete verification environment.

The user could force the simulation to quit via a `vmm_fatal macro or proceed with the simulation for a particular checker instance failure. The use of vmm_log for assertion error messaging gets recognized by the VMM environment leading to an effective simulation result. Integration of VMM messaging service provides extended flexibility to the user to control the simulation based on the severity of the checker instance.

Steps to integrate vmm_log with assertion reporting

· Declaration of a new package with a static VMM log object

package vmm_sva;

`include “vmm.sv”

vmm_log sva_vmm_log = new(“SVA_CHECKER”,$psprintf(“%m”));

endpackage : vmm_sva

· Inclusion of the package in the assertion file

module sva_file(….)

import vmm_sva ::*;

// AHB master property check

property HburstSingleHtransNseq;

@ (posedge HCLK)disable iff (!HRESETn) (

((SINGLE && HGRANT)

)

|-> ((NSEQ || IDLE)));

endproperty

HburstSingleHtransNseq_check  : assert property (HburstSingleHtransNseq)

else `vmm_fatal (sva_vmm_log, “AMBA Compliance Protocol Rules : ERRMSINGLE: Master has issued a SEQ/BUSY type SINGLE transfer”));

endmodule

Simulation Result:

Bases on the severity of the assertion, you could terminate the simulation and also the testbench environment recognizers this failure and qualifies the simulation as a failure as depicted below

*FATAL*[FAILURE] on SVA_CHECKER(vmm_sva) at                  195:

[AMBA Compliance Protocol Rules : ERRMSINGLE]   Master has issued a SEQ/BUSY type SINGLE transfer

Simulation *FAILED* on /./ (/./) at                  195: 1 errors, 0 warnings

$finish called from file “/tools/eda/snps/vcs-mx/etc/rvm/vmm.sv”, line 36499.

$finish at simulation time                  195

V C S   S i m u l a t i o n   R e p o r t

Users can choose from the variety of vmm_log macros such as `vmm_error, `vmm_warning etc. to suit the relevant message being flagged by that assertion. With this subtle change/enhancement to the SVA action block one can leverage on VMM’s simulation controllability features such as error counting, simulation handling of errors (stop, debug, continue etc.). One can also promote/demote errors to warnings for instance.

A final note on the logger instance being shown in this example: while the above shown code works, typical usage would classify the messages originating from different portions of design/verification into individual logger instances.

In our next entry in this series, we will address the second aspect of observability – i.e. tie the results to Verification plan, so stay tuned!

Srinivasan Venkataramanan, CVC Pvt. Ltd.

Abhishek Muchandikar, Sr RnD Engineer, Verification Group, Synopsys

Sadanand Gulwadi, Sr. Staff CAE, Verification Group, Synopsys Inc., Mt. View, CA, USA

Assertions for protocol checking has been popular for quite some time now. With several off-the-shelf assertion/monitor IPs available from EDA vendors and providers such as CVC (www.cvcblr.com), end users need not have to spend too much time thinking about what assertions to add in their designs, how to code them etc. All that users would need to do is to create suitable bind files and off they go!

While using assertions sounds simple and straightforward, there are scenarios for which users need to watch out. The methodology of using assertions and leveraging on assertion indications from simulations is vital for ROI of Assertion Based Verification. There are several assertion coding guidelines available with VMM book – infact a whole chapter is dedicated to writing effective assertions (Chapter-3, see: http://www.springer.com/engineering/circuits+%26+systems/book/978-0-387-25538-5).

VMM also provides guidelines on how to integrate assertions errors via standard messaging route such as `vmm_error. An additional methodology note that we developed while working with a large DSP customer is to identify quickly “totally vacuous” assertions in a simulation run.

For example, if assertions did fire, then you have likely found a bug. However if assertions remained silent throughout a simulation, then you cannot afford to be too happy, for the assertions may have been “totally vacuous”. This is a term that my ex-colleague and I coined during our work at a large DSP customer here. They were adding assertions and looking for improved productivity early on rather than having to go through detailed assertion coverage metrics, various dump files, and so forth at a later stage While standard garden variety vacuity is quite well understood and explained in our regular SVA trainings (SVA Trainings), the concept of “totally vacuous” is a step beyond that. Totally vacuous assertions are those that were *never* successful during the entire simulation run. This can be due to a few reasons:

1. The assertions were never attempted at all (perhaps the CLOCK was undriven, or was part of a gated clock of a low power domain etc.)

2. The antecedent of a property was never satisfied etc.

Further, observation of the assertion behaviour stated above might indicate the following potential issues in your design or verification plan:

1. Incorrect clock network connections, clock enables, and so forth.

2. Test-case is weak and does not address a key portion of your design (a coverage hole).

For instance, consider the following assertion (taken from our SVA handbook, www.systemverilog.us/sva_info.html)

/* Behavior: if the transfer type is BUSY then on the corresponding

data transfer , the slave must provide a zero wait state OKAY response

(default clock) */

property pResponseToBusyMustBeZeroWaitOKAY (hResp,hReady,hTrans);

@(posedge hclk) (((hTrans == BUSY) && (hReady == 1)) |->

##1 ((hResp == OKAY) && (hReady == 1)) );

endproperty: pResponseToBusyMustBeZeroWaitOKAY

Consider the case when the stimulus didn’t drive the hTrans to be BUSY throughout the simulation. This is strange and means that the stimulus is weak. However when (and how) does a user find this out? With the usual wisdom of “No news is GOOD news”, it is very easy to ignore this important coverage hole and move on with other work. However, the customer desired such strange assertion behaviour to be flagged as early as possible – at the end of every simulation run.

VCS does have the ability to catch such “totally vacuous” assertions and accordingly reports the following at the end of a simulation run:

**** Following assertions did not fire at all during simulation. *****

“/proj/cvc_mips/ahb_mip/master.sva “, 48:

a_pResponseToBusyMustBeZeroWaitOKAY: Antecedent was never satisfied

“/proj/cvc_mips/ahb_mip/slave.sva “, 32:

a_pLowPowerGclk: No attempt started

The above output is default in VCS without the need for any additional user-driven options and frees the user from the additional steps of enabling assertion coverage, debug, etc. Assertion coverage and debug are indeed powerful features for analyzing problems, but should be turned on only after ensuring the assertions are not “totally vacuous” – a glaring weakness that requires being flagged early on by default. It is all about productivity at the end of the day – if a tool can help improve productivity it is always welcome

So the next time VCS prints such a message, you had better watch out before calling it a day!