How do I seertion for this condition?

SystemVerilog
, ,
1

Hello,

I am trying to write an assertion for the following specification.

ack must arrive within 8 clocks.
$rose(req) must not arrive more than 3 times before ack arrives.

Not able to write a correct assertion.

Thanks much.

2

In reply to ashokmehta72:

ack must arrive within 8 clocks from 1sr rose(req).
$rose(req) must not arrive more than 3 times before ack arrives.

You need support logic to exclude new $roses from the 1st one. Below is pseudo-code.

 
bit lock;
function void setlock(bit v);
  lock=v;
-----

assert property(($rose(req) && lock==0, setlock=1) |-> 
      ##[1:8] ack) setlock=0; else setlock=0; // reset the lock
//pass or fail
// $rose(req) must not arrive more than 3 times before ack arrives
assert property($rose(req) && lock==0 ¦=> ($rose(req)[=1]) [*0:2] ##1 ack);

Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Thanks

4

In reply to ash72:

You may want to consider


assert property(($rose(req) && lock==0, setlock=1) |-> 
      ##[1:8] ack) setlock=0; else setlock=0; // reset the lock

I updated the previous reply 
// $rose(req) must not arrive more than 3 times before ack arrives
// I had the right concept, but the wrong variable 
assert property($rose(req) && lock==0 ¦=> ($rose(req)[=1]) [*0:2] ##1 ack);
// b[=m]  is equivalent to (  b [->m] ##1 !b [*0:$] )
// b[->m] is equivalent to ( !b [*0:$] ##1 b)[*m]