How to pass delay through a variable in assertion

SystemVerilog
1

Hi,

I have to pass fixed delay but through the variable as it is coming from some another signal.

example

delay = sig1/2;//// sig1 can be 3 or 4 or 5 any value at one time
property delay_check_device;
bit [3:0] w_delay;
@(posedge clk)
disable iff (!rst_n)
(((w_trig) && (req==1)),w_delay= (delay+1’b1)) |-> (w_delay>0, w_delay=w_delay-1’b1)[*0:$] ##1 w_delaylat==0 ##0 (ack == 1);///tried with logic but it is not working
//(w_trig == 1) && (req == 1)|-> ##<3> (ack=='d64);/// want logic to behave as this code behave the only thing needed is local variable w_delay in place of 3 which is coming from delay variable.
endproperty

Thanks

2

In reply to myselfprakhar:

hey prakhar,
try this one


property @(posedge clk)
  int w_delay;
  ((w_trig && req==1), w_delay= delay+1'b1) |-> (w_delay>0, w_delay=w_delay-1'b1)[*0:$] ##0 w_delay==0 ##0 (ack == 64);

endproperty
3

In reply to mukeshkumar.saha@reliabletechsys.com:

Hi Mukesh,

I used the above logic, but I am getting the error near “==”: syntax error, unexpected ‘==’ for w_delay==0 and if I am using
((w_trig && req==1), w_delay= delay+1’b1) |-> (w_delay>0, w_delay=w_delay-1’b1)[*0:$] ##0 w_delay=0 ##0 (ack == 64);
I am getting the error near “=”: syntax error, unexpected ‘=’

4

Hi,

The below code worked:

property prop;
int w_delay;
@(posedge clk)
((w_trig && req==1), w_delay= delay+1’b1) |-> (w_delay>0, w_delay=w_delay-1’b1, display("w_delay=%0d",w_delay))[*0:] ##0 w_delay==0 ##0 (ack == 1);
endproperty

P1: assert property(prop) $info(“KING Assertion pass”);
else $error(“KING Assertion fail”);

Regards,
Dilip

5

In reply to Dilip Bagadi:

Thanks Dilip, the code is working…

6

In reply to myselfprakhar:

((w_trig && req==1), w_delay= delay+1’b1) |-> (w_delay>0, w_delay=w_delay-1’b1, display("w_delay=%0d",w_delay))[*0:] ##0 w_delay==0 ##0 (ack == 1);
Is of the form
a |-> b[*0:$] ##0 c;
From my book “[1] An empty sequence fused with a sequence is empty. An empty sequence is a sequence that uses the 0 as the repetition number, such as a[*0]. For a sequence overlapping to match, the one cycle overlap must exist in both sequences. In other words, if either of the two sequences have an empty match, then there cannot be an overlap because one of the two sequences is of zero length. Thus, an empty sequence fused with any sequence results in no match.”

a |-> b[*0:$] ##0 c;  is same as
a |-> b[*0] ##0 c   or  // <-- this always results to 0 (a fail) 
      b[*1] ##0 c   or 
      ... 
      b[*n] ##0 c  
Thus, Is is recommended that you change this 
FRoM   a |-> b[*0:$] ##0 c; 
TO     a |-> b[*1:$] ##0 c; 
or TO  a |-> b[*0:$] ##1 c;
7

hi ben,can i access the global variable which is declared in the assertion module in the property and endproperty ,if yes then can i access the config class variables in the property and endproperty.

8

Are you talking about accessing a local property variable for external use?
If so, the answer is NO.
What are your goals here? why do you ask that question?
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.