Home > Community > Forums > Functional Verification > PSL endpoints and ended()

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

 PSL endpoints and ended() 

Last post Tue, Oct 3 2006 5:50 PM by archive. 12 replies.
Started by archive 03 Oct 2006 05:50 PM. Topic has 12 replies and 2653 views
Page 1 of 1 (13 items)
Sort Posts:
  • Tue, Oct 3 2006 5:50 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    PSL endpoints and ended() Reply

    I need to write a property that states if conditon A occurs then SeqA or SeqB must have occured.

    The PSL built-in ended() is not supported in IFV 5.7-s5.  So, I can't do either of these:
    always {A} |-> {ended(SeqA) | ended(SeqB)}
     
    never (A & ~(ended(SeqA) | ended(SeqB))

    Also, I get this error when calling SeqA and SeqB endpoints.
    endpoint SeqA ...
    endpoint SeqB ...

    always {A} |-> {SeqA | SeqB}
                       |
    "Endpoints and sequences are illegal as verilog operands."

    Does anyone have another idea how this can be done?

    Thanks,

    Ross



    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Tue, Oct 3 2006 8:04 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

     Perhaps

    // psl endpoint SeqA = {p; q};

    // psl endpoint SeqB = {r ;s};

    // psl assert always ({a} |-> {{SeqA} | {SeqB}});

    will work.

    Explicitly have braces to identify that the | is a sequence or operator and not a verilog or operator.  


    Originally posted in cdnusers.org by vtaylorcva
    • Post Points: 0
  • Tue, Oct 3 2006 10:59 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    You can solve this problem by using "satellite" HDL-Code: define a HDL-signal which becomes active, if SeqA ends and define a HDL-signal which becomes active if SeqB ends. Then you can use these signals in your PSL-Assertion. Because I guess there is some time needed until the end of SeqA or SeqB you have to insert some "time" by using "[*]":
    always {A} |-> {[*];sig_if_SeqA_ends | sig_if_SeqB_ends}
    Hope this helps,
    Matthias


    Originally posted in cdnusers.org by Matthias Schweikart
    • Post Points: 0
  • Wed, Oct 4 2006 8:28 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    Thanks,

    This works:
    //psl assert always( {a} |-> {{SeqA} | {SeqB}} )@(posedge clk);

    This still gets the error:
    //psl assert never( {a} & ~({SeqA} | {SeqB}) )@(posedge clk);
                                    |
    ncvlog: *E,PSVERO (test.v,9|32): Endpoints and sequences are illegal as verilog operands.  Check sequence composition syntax.

    I guess I'll go with the always...


    Originally posted in cdnusers.org by weberrm
    • Post Points: 0
  • Mon, Oct 9 2006 2:53 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    I think it would be very usefull to support enpoints (or ended() ) as a boolean in the modeling layer of PSL. That way, a PSL-sequence endpoint can trigger a VHDL/Verilog process. It would also create a "workaround" for (SV-)action-block like behavior.


    Originally posted in cdnusers.org by stijn
    • Post Points: 0
  • Mon, Oct 9 2006 11:15 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    I think that the "endpoint" in PSL has been dropped from the latest IEEE standard. We have it in our parser for backwards compatibility.

    The "ended()" function from the PSL standard takes a sequence as a parameter and returns a boolean as a result. Here is the code from a sample Vunit file that I put together to observe the behavior when support for the ended() function first came out in IUS 5.7.

    vunit testended ( testit ) {
    default clock = posedge clk;
    sequence abc_seq = { a; b; c }@(posedge clk);
    p_ended: assert always { ended(abc_seq) } |=> { d };
    endpoint abc_ep = { a; b; c };
    p_endpt: assert always abc_ep -> next d;
    always @(posedge ended(abc_seq)) $display($time,,"a;b;c has ended");
    wire y;
    assign y = ended(abc_seq);
    }

    So, you can use "ended()" in a property or sequence and pass it a sequence name. You can use it to affect the HDL behavior. The rest of the discussion here seems to be around syntax issues, making sure that you use sequences where sequences are legal and booleans where they are legal. Keeping you parentheses and braces correct can be confusing, but it is necessary.


    Originally posted in cdnusers.org by TAM
    • Post Points: 0
  • Mon, Oct 9 2006 11:48 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    Thans for your reply, I was using ius5.6 until recently wher ended() was not supported and endpoint could not be assigend to a signal (boolean). I will retry with 5.7 and ended().


    Originally posted in cdnusers.org by stijn
    • Post Points: 0
  • Tue, Oct 10 2006 12:14 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    Me again.
    I tried what you proposed (but using VHDL) with IUS 5.7-p001. I doesn' t work :
    in my vunit I have :
    sequence spi_transfer_start is {fell(spi_e_csn)} ;
    signal spi_transfer_start_cycle : boolean;
    spi_transfer_start_cycle <= ended(spi_transfer_start);

    When I compile it gives :

    ncvhdl: 05.70-p001: (c) Copyright 1995-2006 Cadence Design Systems, Inc.
    spi_transfer_start_cycle <= ended(spi_transfer_start);
    |
    ncvhdl_p: *E,IDENTU (/projects/erip/eripsae/SPI_E/VHDL/spi_e.psl,689|32): identifier (ENDED) is not declared [10.3].
    make: *** [/projects/erip/eripsael/SPI_E/LIB/spi_e/entity/pc.db] Error 1
    make: Target `VHDLTOP' not remade because of errors.


    Is there no support (forseen?) for ended() in the VHDL-flavor of PSL? Or am I missing something?

    Thanks,

    Stijn


    Originally posted in cdnusers.org by stijn
    • Post Points: 0
  • Tue, Oct 10 2006 12:19 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    Hi,

    I guess your problem is that you wnat to assign an endpoint to a signal outside of a property. Afaik ended can only be used in the context of an assertion. Your assignment is not in this context.

    Joerg.


    Originally posted in cdnusers.org by jmueller
    • Post Points: 0
  • Tue, Oct 10 2006 12:27 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    Joerg,

    In TAM's example, there is an assignement outside a property which appears to work :


    wire y;
    assign y = ended(abc_seq);


    I expect ( and want to use) the same in VHDL.

    Stijn


    Originally posted in cdnusers.org by stijn
    • Post Points: 0
  • Tue, Oct 10 2006 12:31 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    Hmm, right, but he is using it inside a vunit. Are you using it outside of a vunit?


    Originally posted in cdnusers.org by jmueller
    • Post Points: 0
  • Tue, Oct 10 2006 12:36 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    I am using it inside a vunit.
    I also check the cds_assertions stubs-file in the cadence installation directory (where functions as prev, next,.. are defined). ended() is not defined in there.

    Stijn


    Originally posted in cdnusers.org by stijn
    • Post Points: 0
  • Tue, Oct 10 2006 6:27 AM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: PSL endpoints and ended() Reply

    I just received confirmation that this is not supported in VHDL, see also the KPNS in the 5.82 release:

    http://sourcelink.cadence.com/docs/files/Release_Info/Docs/abvKPNS/abvKPNS5.82/abvKPNS.html#1011834

    I recommend that you contact your support person and have him file a PCR or log a service request through sourcelink.

    Nevertheless, the endpoint syntax still works, even in VHDL.

    Regards,
    Joerg.


    Originally posted in cdnusers.org by jmueller
    • Post Points: 0
Page 1 of 1 (13 items)
Sort Posts:
Started by archive at 03 Oct 2006 05:50 PM. Topic has 12 replies.