Velocity Reviews - Computer Hardware Reviews

Velocity Reviews > Newsgroups > Programming > VHDL > New PSL standard

Reply
Thread Tools

New PSL standard

 
 
HT-Lab
Guest
Posts: n/a
 
      04-30-2010
For those that haven't seen it.....


This week the IEEE announced approval of the revised IEEE 1850T, "Standard for
PSL: Property Specification Language." This EDA standard provides a language for
formal specification of electronic system behavior.

The standard is based on the PSL standard originally developed by Accellera. PSL
was transferred to the IEEE and was first published by the IEEE in 2005.

IEEE 1850-2009 helps hardware developers reduce verification time and costs. The
IEEE 1850 Working Group collaborated with four other hardware language projects
to support cross-language properties. The other projects are IEEE P1076T, IEEE
Standard VHDL; IEEE P1364T, Standard for Verilog Hardware Description Language;
IEEE P1647T, Standard for the Functional Verification Language 'e'; and IEEE
P1800T, Standard for SystemVerilog Hardware Description Language.

For more information about this important verification standard, please visit
www.eda.org/ieee-1850/.

If you are interested in joining Accellera and contributing to and participating
in our EDA and IP standards efforts, please email http://www.velocityreviews.com/forums/(E-Mail Removed).


Best Regards,

Shrenik Mehta
Accellera Chair

Does anybody know what has been added/changed?

Hans
www.ht-lab.com


 
Reply With Quote
 
 
 
 
Amal
Guest
Posts: n/a
 
      05-01-2010
On Apr 30, 3:11*am, "HT-Lab" <(E-Mail Removed)> wrote:
> For those that haven't seen it.....
>
> This week the IEEE announced approval of the revised IEEE 1850T, "Standard for
> PSL: Property Specification Language." This EDA standard provides a language for
> formal specification of electronic system behavior.
>
> The standard is based on the PSL standard originally developed by Accellera. PSL
> was transferred to the IEEE and was first published by the IEEE in 2005.
>
> IEEE 1850-2009 helps hardware developers reduce verification time and costs. The
> IEEE 1850 Working Group collaborated with four other hardware language projects
> to support cross-language properties. The other projects are IEEE P1076T, IEEE
> Standard VHDL; IEEE P1364T, Standard for Verilog Hardware Description Language;
> IEEE P1647T, Standard for the Functional Verification Language 'e'; and IEEE
> P1800T, Standard for SystemVerilog Hardware Description Language.
>
> For more information about this important verification standard, please visitwww.eda.org/ieee-1850/.
>
> If you are interested in joining Accellera and contributing to and participating
> in our EDA and IP standards efforts, please email (E-Mail Removed).
>
> Best Regards,
>
> Shrenik Mehta
> Accellera Chair
>
> Does anybody know what has been added/changed?
>
> Hanswww.ht-lab.com


How does PSL compare to SVA? Any advantages/disadvantages of using
one or the other? Silly question: Why do we need two language I
wonder! Well I guess the same reason we have two major HDL
languages. Syntax/personal Preference? Well, I understand each HDL's
strengths and weaknesses, but can you elaborate on the differences
between SVA and PSL?

-- Amal
 
Reply With Quote
 
 
 
 
Jonathan Bromley
Guest
Posts: n/a
 
      05-01-2010
On Fri, 30 Apr 2010 17:42:49 -0700 (PDT), Amal wrote:

>How does PSL compare to SVA? Any advantages/disadvantages of using
>one or the other? Silly question: Why do we need two language I
>wonder! Well I guess the same reason we have two major HDL
>languages. Syntax/personal Preference? Well, I understand each HDL's
>strengths and weaknesses, but can you elaborate on the differences
>between SVA and PSL?


PSL came first, as the standardisation of IBM's "Sugar". Some while
later, as SystemVerilog assertions were being developed from their
original basis in Vera assertions, the decision was made (brilliant
choice in my opinion) to bring the semantics of SV assertions in
to line with PSL. But the SVA syntax was of course crafted to
make SV assertions fit smoothly into SystemVerilog, whereas
PSL was always thought of as a separate language that could
"borrow" boolean-expression syntax from whatever language
it was used with (Verilog, VHDL, GDL).

PSL has some heavy-duty features for formal verification that
don't really make sense in SVA, because SVA is integrated as
part of a language that's defined by its simulation behaviour;
so any construct that's not simulation-friendly makes little
sense in SVA. I'm thinking here of the branching temporal
logic stuff (CTL, Computational Tree Logic).

SVA has some important and useful features - notably local
variables in properties - that were not originally part of PSL.
(I heard a rumour that the new version of PSL has them, but
I haven't studied it.) There are ways to get around the
lack in PSL, but I find local variables much more intuitive
than the PSL alternatives (%for etc.) SVA also has some
simulation-only features (task call on success of a property)
that make no sense for users of formal tools. I guess you
could argue that this pollutes the elegance and rigour of
SVA, but it's too useful to lose!

PSL also has a rather elegant Linear Temporal Logic syntax
that is particularly good for expressing certain types of
assertion; it didn't exist in the original form of SVA, which
is based entirely on a temporal sequences syntax. But
SystemVerilog-2009 has added most of the PSL-style
LTL operators - it wasn't a big deal to do that, because
all the necessary core functionality was already there.

Both languages have a rich set of features for parameter-
isation of properties, and all the temporal operators you're
likely to need. Both are robustly and precisely defined
by a rigorous temporal algebra that, for me, lives somewhere
on a scale from Difficult to Haven't A Clue. For the huge
majority of practitioners, it's fair to say that anything you
can do in one language can be done equally well in the other.

So, in summary:
- if you care about sophisticated formal property
checking, you may want the CTL features of PSL;
- if you're a SystemVerilog simulation user, it's an
obvious no-brainer to use SVA because it integrates
so much more smoothly with the language syntax;
- if you're a VHDL simulation user, it's mainly a matter
of personal preference because the tool vendors
make it equally easy to use either SVA or PSL.

Hope this helps!
--
Jonathan Bromley
 
Reply With Quote
 
hssig
Guest
Posts: n/a
 
      05-01-2010
>if you're a VHDL simulation user, it's mainly a matter
> of personal preference because the tool vendors
> make it equally easy to use either SVA or PSL.


If you want to integrate assertions into your VHDL design modules what
is the better solution: PSL or SVA ?

Cheers,
hssig

 
Reply With Quote
 
Jonathan Bromley
Guest
Posts: n/a
 
      05-02-2010
On Sat, 1 May 2010 09:19:26 -0700 (PDT), hssig wrote:

[me]
>>if you're a VHDL simulation user, it's mainly a matter
>> of personal preference because the tool vendors
>> make it equally easy to use either SVA or PSL.


[hssig]
>If you want to integrate assertions into your VHDL design modules what
>is the better solution: PSL or SVA ?


If you want the assertions embedded in the VHDL source,
PSL is probably neater. To use SVA you would need to
create a separate SV module and "bind" it into the VHDL -
easy, but it puts the assertions in a separate source file.
To use PSL you can either embed the PSL code in special
comments beginning "--psl" or, if you're using VHDL-2008
and the tool vendors are supporting this (anyone know?),
you can literally embed the PSL directly in your VHDL.

Of course, the idea of writing the assertions in a
separate file and binding them to your VHDL is also
available with PSL's "vunit" construct.
--
Jonathan Bromley
 
Reply With Quote
 
Paul Uiterlinden
Guest
Posts: n/a
 
      05-03-2010
Jonathan Bromley wrote:

> On Sat, 1 May 2010 09:19:26 -0700 (PDT), hssig wrote:
>
> [me]
>>>if you're a VHDL simulation user, it's mainly a matter
>>> of personal preference because the tool vendors
>>> make it equally easy to use either SVA or PSL.

>
> [hssig]
>>If you want to integrate assertions into your VHDL design modules what
>>is the better solution: PSL or SVA ?

>
> If you want the assertions embedded in the VHDL source,
> PSL is probably neater. To use SVA you would need to
> create a separate SV module and "bind" it into the VHDL -
> easy, but it puts the assertions in a separate source file.
> To use PSL you can either embed the PSL code in special
> comments beginning "--psl" or, if you're using VHDL-2008
> and the tool vendors are supporting this (anyone know?),
> you can literally embed the PSL directly in your VHDL.
>
> Of course, the idea of writing the assertions in a
> separate file and binding them to your VHDL is also
> available with PSL's "vunit" construct.


Thanks for your informative posts!

I am missing one scenario: design in VHDL, verification in SV/OVM.

My guess is that in that scenario SVA would be the better choice. It will
give the verification environment access to coverage bins and what not,
residing in the design. This would make "intelligent" behaviour of the
verification environment possible, like adapting the stimulus generation
steered by functional coverage.

Or is this also possible with PSL?

Until now it's all theory to me, I haven't had any practical experience with
SV/OVM/SVA/PSL.

--
Paul Uiterlinden
www.aimvalley.nl
e-mail addres: remove the not.
 
Reply With Quote
 
HT-Lab
Guest
Posts: n/a
 
      05-04-2010
"Paul Uiterlinden" <(E-Mail Removed)> wrote in message
news:4bdf3c7c$0$22940$(E-Mail Removed)4all.nl...
> Jonathan Bromley wrote:
>
>> On Sat, 1 May 2010 09:19:26 -0700 (PDT), hssig wrote:
>>

...
>>
>> Of course, the idea of writing the assertions in a
>> separate file and binding them to your VHDL is also
>> available with PSL's "vunit" construct.

>
> Thanks for your informative posts!
>
> I am missing one scenario: design in VHDL, verification in SV/OVM.
>
> My guess is that in that scenario SVA would be the better choice.


Embedding PSL in your VHDL is much less verbose than using a SV module with some
SVA assertions and binding that to your VHDL entity/architecture.

> It will
> give the verification environment access to coverage bins and what not,
> residing in the design. This would make "intelligent" behaviour of the
> verification environment possible, like adapting the stimulus generation
> steered by functional coverage.
>
> Or is this also possible with PSL?


AFAIK not with the current standard, but I found the paper below which describes
that bins are now supported in the new 1850 standard:

http://citeseerx.ist.psu.edu/viewdoc...=rep1&type=pdf

I also understand that vunits can now be parameterised,

Hans
www.ht-lab.com


>
> Until now it's all theory to me, I haven't had any practical experience with
> SV/OVM/SVA/PSL.
>
> --
> Paul Uiterlinden
> www.aimvalley.nl
> e-mail addres: remove the not.



 
Reply With Quote
 
hssig
Guest
Posts: n/a
 
      05-04-2010
>
> AFAIK not with the current standard, but I found the paper below which describes
> that bins are now supported in the new 1850 standard:
>


Does that mean that PSL "bins" would allow functional coverage in
simulation tools (as coverage points allow in SVA today)?

cheers,
hssig

 
Reply With Quote
 
Paul Uiterlinden
Guest
Posts: n/a
 
      05-04-2010
HT-Lab wrote:

> "Paul Uiterlinden" <(E-Mail Removed)> wrote in message
> news:4bdf3c7c$0$22940$(E-Mail Removed)4all.nl...
>> Jonathan Bromley wrote:
>>
>>> On Sat, 1 May 2010 09:19:26 -0700 (PDT), hssig wrote:
>>>

> ..
>>>
>>> Of course, the idea of writing the assertions in a
>>> separate file and binding them to your VHDL is also
>>> available with PSL's "vunit" construct.

>>
>> Thanks for your informative posts!
>>
>> I am missing one scenario: design in VHDL, verification in SV/OVM.
>>
>> My guess is that in that scenario SVA would be the better choice.

>
> Embedding PSL in your VHDL is much less verbose than using a SV module
> with some SVA assertions and binding that to your VHDL
> entity/architecture.


Good point.

>> It will
>> give the verification environment access to coverage bins and what not,
>> residing in the design. This would make "intelligent" behaviour of the
>> verification environment possible, like adapting the stimulus generation
>> steered by functional coverage.
>>
>> Or is this also possible with PSL?

>
> AFAIK not with the current standard, but I found the paper below which
> describes that bins are now supported in the new 1850 standard:
>
>

http://citeseerx.ist.psu.edu/viewdoc...=rep1&type=pdf
>
> I also understand that vunits can now be parameterised,
>


Thanks for the pointer. PSL is still growing:

"Over time, we can expect to see an increase in the use of the coverage
capabilities of PSL to enable coverage-driven verification."


--
Paul Uiterlinden
www.aimvalley.nl
e-mail addres: remove the not.
 
Reply With Quote
 
Paul Uiterlinden
Guest
Posts: n/a
 
      05-04-2010
hssig wrote:

>>
>> AFAIK not with the current standard, but I found the paper below which
>> describes that bins are now supported in the new 1850 standard:
>>

>
> Does that mean that PSL "bins" would allow functional coverage in
> simulation tools (as coverage points allow in SVA today)?


There are bins in PSL (from the link posted by Hans):

<quote>
Similarly, the following cover directive would detect any
transaction involving a request from one of 16
components, followed by a grant for the same
component within the specified maximum delay.

cover for i in {0:15}:
{request(i); {grant(i) within [*max_delay]}};

</quote>

However, it is not clear to me how you can read back the result of the bin
in your VHDL code.

--
Paul Uiterlinden
www.aimvalley.nl
e-mail addres: remove the not.
 
Reply With Quote
 
 
 
Reply

Thread Tools

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is On
HTML code is Off
Trackbacks are On
Pingbacks are On
Refbacks are Off


Similar Threads
Thread Thread Starter Forum Replies Last Post
ANN: Project VeriPage Announces New Articles on SystemVerilog, PSL Swapnajit Mittra VHDL 0 06-23-2005 02:26 PM
ANN: Project VeriPage Update - New articles on SystemVerilog and PSL Swapnajit Mittra VHDL 1 05-27-2005 09:07 PM
PSL pros and cons Kumar Vijay Mishra VHDL 2 10-02-2004 12:34 AM
PSL: New 2nd Edition book: Using PSL for formal and dynamic verification ben cohen VHDL 0 01-27-2004 01:09 AM
PSL tutotorial at designcon and dvcon ben cohen VHDL 2 12-21-2003 11:43 AM



Advertisments