Friday, November 21, 2008     Register | Login | Search | Contact Us
     
   
     
     

Many of you already received communications about the move of the Cadence user community into cadence.com. And many of you have already joined, with over 4000 registrations in the first two weeks.

The new Cadence Community enhances the ability of Cadence users to connect and collaborate. In addition to moving the community into cadence.com -- enabling single sign-on for community, Sourcelink and Cadence events -- the new site is organized around nine technology segments, giving you easy access to product information, training, forums and blogs. Some of the new features include:
  • Ability to respond to posts via e-mail
  • Technology-specific blogs
  • Latest Web 2.0 social networking capabilities
  • Public profile options
  • Private messaging
  • Friends lists
Visit the new Cadence Community today at www.cadence.com/community and join the discussions!

Registration note: Due to the scope of the enhancements and the new SSO registration system, we were not able to migrate existing cdnusers.org member accounts. So new registrations are required, but this enables a broader set of functionality we think you'll enjoy.

Forum note: Under the guidance of forum moderators, we have taken the 20+ cdnusers.org forums and consolidated them into 11 forums on the new site. Posts have been brought over so you can leverage that posting history. CDNusers forums will be set to read only starting 7/30, and cdnusers.org will be redirected to the new community on 8/4.

Best regards,
Mike and Tom

Michael A. Catrambone - Steering Committee Chairman
Distinguished Engineer
PCB/Mechanical
UTStarcom, Inc.

Tom Diederich
Cadence Community Manager
Home
Forums
Forums > Functional Verification > Assertion-Based Verification and Formal Analysis

Subject: PSL endpoints and ended()
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
weberrm
Posts: 0
Online: User is Offline
10/03/2006 5:50 PM  
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
vtaylorcva
Posts: 1
Online: User is Offline
10/03/2006 8:04 PM  
 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.  

Matthias Schweikart
Posts: 1
Online: User is Offline
10/03/2006 10:59 PM  
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
weberrm
Posts: 0
Online: User is Offline
10/04/2006 8:28 AM  
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...
stijn
Posts: 5
Online: User is Offline
10/09/2006 2:53 AM  
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.
TAM
Posts: 56
Online: User is Offline
10/09/2006 11:15 AM  
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.
stijn
Posts: 5
Online: User is Offline
10/09/2006 11:48 PM  
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().
stijn
Posts: 5
Online: User is Offline
10/10/2006 12:14 AM  
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 ⎖.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
jmueller
Posts: 0
Online: User is Offline
10/10/2006 12:19 AM  
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.
stijn
Posts: 5
Online: User is Offline
10/10/2006 12:27 AM  
Joerg,

In TAM's example, there is an assignement outside a property which appears to work :
[quote]
wire y;
assign y = ended(abc_seq);
[/quote]

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

Stijn
jmueller
Posts: 0
Online: User is Offline
10/10/2006 12:31 AM  
Hmm, right, but he is using it inside a vunit. Are you using it outside of a vunit?
stijn
Posts: 5
Online: User is Offline
10/10/2006 12:36 AM  
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
jmueller
Posts: 0
Online: User is Offline
10/10/2006 6:27 AM  
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.
Posting to forums is available to community members only.
Login or Register


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.