New PSL standard

Discussion in 'VHDL' started by HT-Lab, Apr 30, 2010.

  1. HT-Lab

    HT-Lab Guest

    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 .


    Best Regards,

    Shrenik Mehta
    Accellera Chair

    Does anybody know what has been added/changed?

    Hans
    www.ht-lab.com
     
    HT-Lab, Apr 30, 2010
    #1
    1. Advertising

  2. HT-Lab

    Amal Guest

    On Apr 30, 3:11 am, "HT-Lab" <> 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 .
    >
    > 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
     
    Amal, May 1, 2010
    #2
    1. Advertising

  3. 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
     
    Jonathan Bromley, May 1, 2010
    #3
  4. HT-Lab

    hssig Guest

    >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
     
    hssig, May 1, 2010
    #4
  5. 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
     
    Jonathan Bromley, May 2, 2010
    #5
  6. 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.
     
    Paul Uiterlinden, May 3, 2010
    #6
  7. HT-Lab

    HT-Lab Guest

    "Paul Uiterlinden" <> wrote in message
    news:4bdf3c7c$0$22940$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/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


    >
    > 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.
     
    HT-Lab, May 4, 2010
    #7
  8. HT-Lab

    hssig Guest

    >
    > 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
     
    hssig, May 4, 2010
    #8
  9. HT-Lab wrote:

    > "Paul Uiterlinden" <> wrote in message
    > news:4bdf3c7c$0$22940$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/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
    www.aimvalley.nl
    e-mail addres: remove the not.
     
    Paul Uiterlinden, May 4, 2010
    #9
  10. 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.
     
    Paul Uiterlinden, May 4, 2010
    #10
  11. HT-Lab

    HT-Lab Guest

    On May 4, 9:30 pm, Paul Uiterlinden <> wrote:
    > 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.


    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 Uiterlindenwww.aimvalley.nl
    > e-mail addres: remove the not.
     
    HT-Lab, May 5, 2010
    #11
  12. HT-Lab wrote:

    > On May 4, 9:30 pm, Paul Uiterlinden <> wrote:


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

    --
    Paul Uiterlinden
    www.aimvalley.nl
    e-mail addres: remove the not.
     
    Paul Uiterlinden, May 5, 2010
    #12
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. ben cohen
    Replies:
    2
    Views:
    563
    annytom
    Dec 21, 2003
  2. ben cohen
    Replies:
    0
    Views:
    791
    ben cohen
    Jan 27, 2004
  3. Kumar Vijay Mishra

    PSL pros and cons

    Kumar Vijay Mishra, Sep 29, 2004, in forum: VHDL
    Replies:
    2
    Views:
    2,598
    vhdlcohen
    Oct 2, 2004
  4. Swapnajit Mittra
    Replies:
    1
    Views:
    515
    Swapnajit Mittra
    May 27, 2005
  5. Swapnajit Mittra
    Replies:
    0
    Views:
    493
    Swapnajit Mittra
    Jun 23, 2005
Loading...

Share This Page