Arbiter Req and Grant

SystemVerilog
1

HI All,

I have an arbiter scenario. When req is present, gnt should come after 4 cycles.
Req ##4 Gnt

This works fine. But, when Req=0, assertion will fail because of ## operator.
I do not want assertion to fail when Req=0.

Could you please help me in writing assertion for this requirement?

Thank You,

2

You need to be more specific what you mean by “when req is present” and
“gnt should come”. Usually this means when the signal first gets asserted or rises (if active high).

  assert property ( @(posedge clk) $rose(req) |-> ##4 $rose(gnt) );
3

Thank you for the reply Dave.

one more query:

assert property ( @(posedge clk) $rose(req) |-> ##4 $rose(gnt) );

This will pass since our design expect 4 clk cycles for gnt.

assert property ( @(posedge clk) $rose(req) |-> ##5 $rose(gnt) );

This will fail since it violates the above condition

Now, I am creating a cover for this scenario.

cover property ( @(posedge clk) $rose(req) |-> ##5 $rose(gnt) );

This cover suppose to fail right? but its passing for all cycles of N.

I wanted to understand: if assert is getting failed for 5 clock cycles, cover is getting pass?
In what case, the cover will fail here?

Thank You,

4

It is a bad coding style to use an implication operator in cover-s - for the exact reason as you’ve experienced, these are called vacuous successes in SVA and a cover usually does not differentiate between vacuous and non-vacuous. For cover - 2 approaches:

  1. Your simulator may already do this internally, check for flags
  2. Rewrite without implication operator, just use ##4 in your example
5

Thank You Srini.

  1. assert property ( @(posedge clk) $rose(req) |-> ##4 $rose(gnt) );
  2. cover property ( @(posedge clk) req ##4 gnt);

Here, 1 and 2 are performing the same functionality.
2nd may not be required in this context.

In general, when to write cover property.
For example, If it is FIFO, then “buffer can get FULL and then empty again”. For this requirement, I can use cover instead of assert since FULL followed by EMPTY involves many write operations followed by read, so basically when there is some sequence is involved, we will choose “cover” instead of “assert”.

In this Arbiter example, I was not able to think where “cover” can be used becuase I do not see any sequence. If possible, can you give one best example for cover in any generic arbiter.

Thank You