SVA : Property is a tautology

SystemVerilog
, , , ,
1

Hi,

I have hooked up the following assertion to an arbiter

property p_req_to_grant(clk,rst,req,gnt);
  @(posedge clk) disable iff (rst)
  req |-> ##[0:$] gnt;
endproperty

ap_req_to_grant_0 : assert property(p_req_to_grant(clk,ares,req[0],grant[0]));

Basically I just want to check that a grant should come ‘eventually’ for any request.

I am getting this warning that
Warning-[SVAC-TAUT] Property is a tautology .
Property is a tautology. Please correct the assertion and try again.

In a given implementation, It may never happen that grant does not come for a request. But why is this property itself a tautology?

Thanks,
Vivek

2

The assertion is unbounded. It will never fail in any simulation. If the req is asserted, then it will wait for infinite time for gnt to get asserted. When req is asserted, it will wait for even 1000 clocks (till end of simulation) for gnt to get HIGH. So, the sequence is true by it’s logic/virtue itself.

You may want to add a bounding condition to your assertion like following sample:

`define MAX_GNT_DELAY 1000
property p_req_to_grant(clk,rst,req,gnt,int n);
  @(posedge clk) disable iff (rst)
  req |-> ##[*0:n] gnt;
endproperty

assert property(p_req_to_grant(clk,ares,req[0],grant[0], `MAX_GNT_DELAY));

For more details, please refer to Section-6.10 of this book.

3

In reply to sharvil111:
Actually, all you need is to make the consequent sequence strong


property p_req_to_grant(clk,rst,req,gnt);
  @(posedge clk) disable iff (rst)
  req |-> strong(##[0:$] gnt);
endproperty
ap_req_to_grant_0 : assert property(p_req_to_grant(clk,ares,req[0],grant[0]));

From my SVA book: Guideline: Qualify as strong properties that are sequences and have range delays or consecutive repetition operators (e.g., [*, [->, [= ) and are consequents in an assertion. This is important when it is necessary to qualify an assertion as a failure if the consequent never terminates at the end of simulation (e.g., with a $finish). Example:

ap_ab_recommend: assert property(@ (posedge clk) a |-> strong([1:$] b)); //GOOD 
ap_ab_weak: assert property(@ (posedge clk) a |-> ([1:$] b)); // weak property 
ap_abc_recommend: assert property(@ (posedge clk) a |-> strong(b[*) ##1 c); // Strong property 
ap_abc_weak: assert property(@ (posedge clk) a |-> (b[*) ##1 c); // weak property

Tools may have a switch such that on finish, you can qualify what the simulator should do. You can specify things like ask, stop, exit.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

4

In reply to ben@SystemVerilog.us:

I agree about ‘strong’ qualifier. Also, there can be usage of ‘s_eventually’ over here.

assert property (@(posedge clk) req |-> s_eventually gnt);

Refer to this PDF for more alternatives.

5

In reply to sharvil111:

Thanks for the explanation !!

6

In reply to ben@SystemVerilog.us:

@sharvil11 and Ben Cohen
Thanks for the solution.

I have one query here. If a req doesn’t get grant at end of simulation, it will be flagged as failure.
But how will a formal tool treat this case ? Can it fail this property and provide a trace because it can still be said that grant may occur in future.

Regards,
Vivek

7

In reply to vivek3016:

I think it formal tool will also fail since it mostly follows pessimistic approach. But I am not sure about it since I am not much familiar with formal tool approaches.

8

I have a situation wherein req comes @(posedge) of clk, but gnt comes at positive duty cycle

clk |-||-||-||-||-||-||-| …

req ___________|-------------------

gnt __________________|---------------

How to write an assertion for such a scenario?

Thanks

9

In reply to foxtrot:

WHy do you think that the following will not work?


assert property (@(posedge clk) req |-> s_eventually gnt);

Also, when you say gnt comes at positive duty cycle, you mean in the middle of a cycle. But will it miss the clk sampling @(posedge clk)? If so, you’ll need to latch the gnt so that it can be sampled.
Note that the following solution could work.


assert property (@(posedge clk) req |-> @ (posedge gnt) 1'b1);

In general, SVA is used with clocking event s sampling data. The above uses the gnt as a clocking event; it is an unusual solution.
Ben

10

In reply to ben@SystemVerilog.us:

This solution is giving me UE results when req and gnt are high?

11

In reply to foxtrot:

UE? Undefined End?
In any case, the @ (posedge gnt) 1’b1)
requires a positive transition on gnt.
If none, then you would get a not finished assertion.

12

In reply to ben@SystemVerilog.us:

I see gnt getting asserted on the 4th clock(after req occurs) in the positive duty cycle. I don’t understand why I see Under Evaluation in my waveform.

13

In reply to foxtrot:
You might see Under Evaluation in the waveform in the attempted threads that are waiting for a gnt.