Pragmatic choice of ABV language - PSL still shines better than SVA

 

As many of our readers would recall, CVC first became very visible to the industry with our early contribution to the assertion-based verification (ABV) via IEEE-1850 PSL (Property Specification Language). Back in 2004 we co-authored our first book on this wonderful language, first of its kind in the temporal assertion languages to become a standard (See our timeline in Facebook for more). Since then it has been a wonderful run of events in this world of functional verification for close to a decade by now.

One of the significant features of PSL has been its simplicity and succinct means of expressing complex temporals through its “Foundation Language” (a.k.a LTL style) subset. We talk about this in detail in our PSL book (http://www.systemverilog.us/psl_info.html). Recently a user came up with a nice requirement at Forum in Verification Academy (See: http://bit.ly/14JTHlI)

The spec goes as follows:

The user attempted a simple SVA 2005 style, but got weird results, then our beloved co-author and guru of assertions, Ben Cohen provided assistance as below (unverified):

Do the same in PSL with FL/LTL style:

Now relate the PSL code back to user spec/requirement:

May be simple, but drives me crazy..

"Req" -> "Gnt" -> "Rel"

When granted, assert if it is going to Idle state before releasing the lock.

Won’t you agree that PSL with its FL/LTL style is lot closer to the spec than the erstwhile SVA-05 sequence based approach?

There is light at the end of tunnel:

1. PSL works well, nice and is usable in all flavors – Verilog, SV, VHDL, SystemC etc.

2. It costs nothing extra in tools – if you have paid for SV, it is very likely you got the PSL too

3. SV 2009 standard did add this LTL features into it, but yet to be supported by many vendors. So your chances of using it in live projects is weak. Of-course push your vendor for it though.

Bottomline – use what works today, PSL is alive & kicking and you’ve already paid for it in your tool. There is hardly any extra learning – if you know one temporal language, the syntax is very similar, so why not get pragmatic and use it!