Stats

  • Locked Locked
  • Replies 7
  • Subscribers 64
  • Views 15552
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

Check if req has ever happened before ack

archive

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.


Originally posted in cdnusers.org by Thomas666

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


    Originally posted in cdnusers.org by vincentr

  • Hi Vince,

    the first case fits my design.

    Thanks.


    Originally posted in cdnusers.org by Thomas666

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


    Originally posted in cdnusers.org by vincentr

  • 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


    Originally posted in cdnusers.org by mavery
    req_ack_eg.pdf

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


    Originally posted in cdnusers.org by Thomas666

  • 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


    Originally posted in cdnusers.org by mavery
    req_ack_eg.pdf

  • Thanks.


    Originally posted in cdnusers.org by Thomas666

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.