PSL pros and cons

[Kumar Vijay Mishra]

Hi.

I would like to know the pros and cons of having Property
Specification Language now offered with ModelSim 6.0. What is its
future? In this respect, what is assertion-based verification (ABV)?
And why all this now?

Thanx in advance.

KVM.

 

[Swapnajit Mittra]

vizziee@yahoo.com (Kumar Vijay Mishra) wrote in message news:<889cd7c9.0409292119.7beccc34@posting.google.com>...

Hi.

I would like to know the pros and cons of having Property
Specification Language now offered with ModelSim 6.0. What is its
future? In this respect, what is assertion-based verification (ABV)?
And why all this now?

Thanx in advance.

KVM.

o What is assertion-based verification?

Assertions 'assert' (or display) when a condition is met or not met. When
you design a logic, essentially you are specifying a list of things that this
logic will do (or, should not do). This way, you can think of a set of
assertions as a mapped version of the specification of the logic. Traditionally,
a logic is checked by running a test that sends out a set of inputs and then
compares the outputs. While this works, for more fine-grain verification, you
define a set of assertions that will check more minute details
during simulation, and/or in a formal environment. (Jury is still out on whether
current set of formal tools are sufficiently capable to solely depend on a
formal methodology.) Most people of the trade believe that a healthy mix
of testcases (directed/random/sweeps) and assertions is a rational
solution for the time being.

Assertions have very good historical data on their side. It is said ~550
bugs were found in DEC alpha using assertions, one of the classic cases
of using assertions. And another 36 or so critical bugs that could not have
been found by regular testcases were found in Pentium using assertions.

o And why all these now?

Assertions are not new. Software programmers have been using assertions
for decades and hardware designers are also using assertions in many forms
for quite some time (DEC alpha comes to mind again). However, few things
did change in last decades. First, towards the middle of 90s, a set of formal
verification tools came up from decades of research in the academia. They
were mostly clumsy and not exactly easy to use, but with time, they have
refined themselves to establish formal verification as a valid proposition.
Secondly, a host of languages emerged with assertion support, starting
with a library for OVL (written using pure Verilog) and then continuing
with Vera (OVA), PSL etc. These languages, arguably, has made the job
easier for a designer to write assertions. Most of the noise that you hear
today about assertions are marketing gimmicks of course, but the
methodology itself is not new and survived so far because of its merit.

HTH,
- Swapnajit.
--
SystemVerilog DPI tutorial on Project VeriPage:
http://www.project-veripage.com/dpi_tutorial_1.php
For subscribing to Project VeriPage mailing list:
<URL: http://www.project-veripage.com/list/?p=subscribe&id=1>

 

[vhdlcohen]

I recommend that you read the postings on the
http://verificationguild.com/
and in particular, "Cost of ABV insertion vs Traditional verification
methods"
http://verificationguild.com/modules.php?name=Forums&file=viewtopic&t=564

That posting had 700 views, and has useful info about assertion-based
verification vs traditional methods discussed by engineers.
Ben
-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
http://www.vhdlcohen.com/ vhdlcohen@aol.com
3107214830@mobile.att.net for Wireless messages < 110-char
Author of following textbooks:
* Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition,
2004 isbn 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn
0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn
0-7923-8115
------------------------------------------------------------------------------

"Hans" <hansydelm@no-spam-ntlworld.com> wrote in message news:<W8Q6d.526$DL6.418@newsfe5-win.ntli.net>...

Hi KVM,

From my limited exposure to the language (I've just done an introduction
course),

Pros:
1) Very powerful formal language, or assert statement on steroid for
hardware engineers
2) Easy to learn, most of the constructs are logical.
3) Most EDA vendors seem to support it.
4) There are even some vendors which can translate your embedded PSL
constructs into hardware monitor.
5) PSL can be embedded in your code (hardware engineer) or put into a
separate vunit (verification engineer).
6) PSL is a full formal language, a subset can be used in dynamic
simulation.

Cons:
1) Only supported by high-end $$$ EDA tools (like Modelsim SE) which will
limit its uptake.
2) During my PSL course I felt that I needed another language to check my
PSL.
3) Easy to create spaghetti code (unreadable constructs).
4) Requires a different mindset, i.e. engineer who do not use assert
statements (other than to stop the simulator) or never heard of OVL will not
use it.
5) They created different flavoured version for VHDL and Verilog, so you can
not write generic PSL. It shouldn't be too difficult to write a translator
between the two flavours but I have seen it yet.
6) Some EDA vendors only support the Verilog flavour

If you want to learn language, get yourself onto a PSL course to make sure
you learn how to think in PSL, secondly get yourself a tool which can
generate VHDL from a drawn waveform, this will enable you to create simple
stimulus for your PSL assertions. Get Ben Cohen's book,

I definitely like the language and will use it for my next design,

Regards,
Hans.
www.ht-lab.com


"Kumar Vijay Mishra" <vizziee@yahoo.com> wrote in message
news:889cd7c9.0409290603.252ba577@posting.google.com...
Hi.

I would like to know the pros and cons of having Property
Specification Language now offered with ModelSim 6.0. What is its
future? In this respect, what is assertion-based verification (ABV)?
And why all this now?

Thanx in advance.

KVM.