Check if req has ever happened before ack > Forums

Forums

Subject: Check if req has ever happened before ack

Posting to forums is available to community members only.
Login or Register

Rate this topic:

Author

Messages

Thomas666
Posts: 7
Online: User is Offline

9/03/2007 2:36 AM
Hi, how to write an assertion, that checks if an acknowledge was requested yet? I think it should look something like: 'assert no_ack_wo_req is always (ack -> prev(req,N));' where N should be 'inf,[*] or [+]' but none of these opportunities seem to work. Thanks.

vincentr
Posts: 6
Online: User is Offline

9/03/2007 3:08 AM
Hi, This depends on the requirement of req with relation to ack: 1. Can req be asserted then removed before ack arrives (and must all req's be ack'd) ? 2. Once asserted, should req remain asserted until ack is received? Depending on which one (1 or 2) is correct for your design will determine the property you need to write. Cheers, Vince.

Thomas666
Posts: 7
Online: User is Offline

9/03/2007 3:33 AM
Hi Vince, the first case fits my design. Thanks.

vincentr
Posts: 6
Online: User is Offline

9/03/2007 3:39 AM
Hi, This is slightly more complex than the 2nd case, and there are more aspects of the problem to consider, but it is possible.... 1. Does every req need to be ack'd, or can some be cancelled/ignored? 2. Will there ever be more than one pending req? i.e. could you get 2 req's before the first ack, and then you you expect 2 acks? Cheers, Vince.

mavery
Posts: 3
Online: User is Offline

9/03/2007 4:25 AM
Hi, These Req/Ack relationships can be more complicated than one may anticipate. Firstly let me say that I do not think that you will be able to do all of the checks that you wish with a single property (because you are actually requiring to check more than one thing) or without using the modeling layer. PSL and SVA cannot "count" things without using modeling layer code. Note that this is subtley different from repetition, which PSL and SVA can both do of course. Attached PDF may answer your question completely or at least in part. BTW, If you are interested in attending a PSL course which deals with practical examples like these then please look at http://www.esperan.com/psl_ov.asp or http://www.cadence-europe.com/education/training/courses.cfm?catID=16 Esperan is fully owned by cadence, in case you were wondering. Mike Avery mavery@cadence.com
Attachment: req_ack_eg.pdf

Thomas666
Posts: 7
Online: User is Offline

9/03/2007 4:29 AM
Hi, the problem is that i have a req_input_array[x:0][y:0] and an ack_output_array[x:0][y:0] and I want to check if there was a corresponding req to an ack. So I have to trigger on the ack. I am sorry, but the req should be asserted until the ack and there won't be more than one req pending for each index. Thanks.

mavery
Posts: 3
Online: User is Offline

9/03/2007 4:37 AM
Hi, These Req/Ack relationships can be more complicated than one may anticipate. Firstly let me say that I do not think that you will be able to do all of the checks that you wish with a single property (because you are actually requiring to check more than one thing) or without using the modeling layer. PSL and SVA cannot "count" things without using modeling layer code. Note that this is subtley different from repetition, which PSL and SVA can both do of course. Attached PDF may answer your question completely or at least in part. BTW, If you are interested in attending a PSL course which deals with practical examples like these then please look at http://www.esperan.com/psl_ov.asp or http://www.cadence-europe.com/education/training/courses.cfm?catID=16 Esperan is fully owned by cadence, in case you were wondering. Mike Avery mavery@cadence.com
Attachment: req_ack_eg.pdf

Thomas666
Posts: 7
Online: User is Offline

Posting to forums is available to community members only.
Login or Register