New PSL standard

[HT-Lab]

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 (e-mail address removed).


Best Regards,

Shrenik Mehta
Accellera Chair

Does anybody know what has been added/changed?

Hans
www.ht-lab.com

 

[Amal]

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 address 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

 

[Jonathan Bromley]

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!

 

[hssig]

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

 

[Jonathan Bromley]

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.

 

[Paul Uiterlinden]

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.

 

[HT-Lab]

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/download?doi=10.1.1.127.1572&rep=rep1&type=pdf

I also understand that vunits can now be parameterised,

Hans
www.ht-lab.com

 

[hssig]

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

 

[Paul Uiterlinden]

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.

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/download?doi=10.1.1.127.1572&rep=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]

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.

 

[HT-Lab]

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.

I suspect using a similar construct to the now obsolete PSL endpoint
(not sure what the 1850 replacement it).

Using the current 1.1 standard you might be able to create simple bins
using endpoints (supported in Modelsim), example:

-- Not tested!
vunit bintest(test(sim))
{

signal count_s : integer:=0;

endpoint n0(boolean clk) is {{request(0); {grant(0) within
[*max_delay]}}}@rose(clk);

process (clk)
begin
if rising_edge(clk) then
if n0(clk)=true then
count_s <= count_s + 1;
end if;
end if;
end process;

}

Hans
www.ht-lab.com

 

[Paul Uiterlinden]

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

I suspect using a similar construct to the now obsolete PSL endpoint
(not sure what the 1850 replacement it).

Using the current 1.1 standard you might be able to create simple bins
using endpoints (supported in Modelsim), example:

-- Not tested!
vunit bintest(test(sim))
{

signal count_s : integer:=0;

endpoint n0(boolean clk) is {{request(0); {grant(0) within
[*max_delay]}}}@rose(clk);

process (clk)
begin
if rising_edge(clk) then
if n0(clk)=true then
count_s <= count_s + 1;
end if;
end if;
end process;

}

Thanks for the example. If I find time to play with PSL bins, I'll use it as
a starting point.