Always property in assertions

SystemVerilog
, , ,
1

Hi,

Lets say I have a requirement that is after I see a ‘request’ then from the next cycle onwards at some point of time I should see a ‘grant’ happening.
Which is straight forward and this is what I currently have:
1)

property (@posedge clk) disable iff (reset)
          request |=> s_eventually grant
endproperty

But when I reviewed some literature online I happen to come across this assertion (for the same requirement):

asserty property (always request |=> s_eventually grant).

Now I have a confusion whether I should make my property like this:
2)

property (@posedge clk) disable iff (reset)
          always request |=> s_eventually grant
endproperty

I was wondering what that always would do here and would 2) be a better way of asserting this requirement when compared to 1).
Thanks for the help.

2

In reply to nipradee:

I’ve never seen always used in the antecedent of an implication. To be true, req must remain high forever. You may be confusing SVA with PSL assertions. They are two different syntaxes.

I think what you want to write is

property (@posedge clk) disable iff (reset)
          $rose(request) |=> request s_until grant;
endproperty

This says for each request, request must remain high until grant, which must happen.

3

In reply to dave_59:

Hi Dave

Thanks for the input. You are right… it was a PSL assertion, just double checked!
Just out of curiosity, in SVA does this assertion:

property (@posedge clk) disable iff (reset)
always request |=> s_eventually grant
endproperty

mean that at every clock we are starting a new thread checking if request is high forever and whose aftermath is that the consequent will never be evaluated? is that correct?
Additionally, is that the reason you told that this SVA assertion is meaningless?

Thanks for the help

4

In reply to nipradee:

Yes, it’ meaningless in that it can never pass. If request rose on the 10th clock cycle and simulation ended just before the 100th clock cycle, you would get 90 failures. But also meaningless in that even if you removed the ‘always’, it would mean only one grant is needed for any number of requests.

5

In reply to dave_59:

Nice catch. Thank you Dave