Clock Delay Range Operator issue in SVA

In reply to ben@SystemVerilog.us:

Hi Ben Cohen,

Thanks for the reply.

I’ve tried above suggestions, I still do not get pass/fail status for checks.

//Tried this. Does not give pass/fail satus
property prop_name(bit [23:0] ADDR_, int POS_);
      @(posedge HCLK) disable iff(!HRESETn)
         first_match( $rose((HTRANS == 2) && (HADDR == ADDR) && !HWRITE) ##1 // $rose needed ??
         !HREADYOUT[*0:16] ##1 (HRDATA[(( ADDR_    - (int' (ADDR_   /4)*4))*8) +: 8] == 8'h55) ##[0:$]
 
         (HTRANS == 2) && (HADDR == ADDR_ + 1) && !HWRITE ##1 
          !HREADYOUT[*0:16] ##1 (HRDATA[(((ADDR_+1) - (int'((ADDR_+1)/4)*4))*8) +: 8] == 8'hAA))
      |->
         ##[1:$] EndLockCheck ##0 Lock[POS_];
endproperty

From your explanation, I know that this is a multi-threaded sequence, but in my simulation, I have only one reads on these AHB addresses, eliminating possibility of starting multi-thread in a property.

Also, consequent signal EndLockCheck goes high after few/200 cycles(That is why I’m using delay of 500 cycles in general). With these hard-coded cycle delays assertion either passes/fails, which is what I need. But when I replace 500 with $ in above checks, SVA does not give any results.

Any other explanation on why checks I wrote should not work might be useful.