Look ma “No RTL, TB, only PSL/SVA – yet I can validate my spec”

It is one of those most commonly asked questions in any assertions training/engagement – assertions describe design behavior, but how can I validate my assertions even before my RTL and/or TB is ready? This is useful for few reasons:

1. Users new to writing assertions using PSL/SVA are expected to make mistakes in assertions initially. So it will be good to get some quick waveforms and validate the assertions in stand alone fashion.

2. While the spec is vague, it creates a mechanism to develop/solidify the spec itself

Typically during the advanced sequences/SEREs section of our PSL (http://www.cvcblr.com/trng_profiles/CVC_LG_PSL_profile.pdf) trainings or SystemVerilog Assertions trainings (http://www.cvcblr.com/trng_profiles/CVC_LG_SVA_profile.pdf) this question invariably comes up.

In principle this is a sweet spot for formal tools (Model checkers) – though not all of them openly promote this nice “hidden gem”. I had first hand experience of doing it via some scripts inside Synopsys not too long ago. But not every user is made aware of this “non-productized” feature.

 

Here is what Jasper had to say on this:

The idea you have mentioned about visualizing assertions in SVA/PSL without DUT/TB has been around within Jasper, for a long while. At that time, one of our customers is trying to train more people within their company to write PSL, and many of the engineers found it easy to write "incorrect PSL", and would like us to provide a tool to help them understand whether the PSL they have written captures the intended behaviors.

I also heard atleast one another EDA vendor confirming its tool being able to easily do this. I will add that name if I get clearance :-)

So as my co-author Ben Cohen (www.systemverilog.us) always insists – YES one can (and perhaps should, for a class of designs/specs) use assertions in SystemVerilog (SVA) and/or PSL during the micro-architecture specification stage itself.

Welcome to the new world of possibilities – true this capability has been around for few years, but I haven’t seen many fully exploiting it yet.