PSL endpoints and ended()

 Perhaps

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

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

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

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.

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.

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

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

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.

Joerg,

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

wire y;
assign y = ended(abc_seq);

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