Assertion implementation

In reply to ben@SystemVerilog.us:

Hi Ben ,

Have 2 questions related to 2nd approach .

(1) What is the LHS for the intersect operator ?

Is it the sequence : *(1, count=count+1)[1:$] ##0 count<4 OR Only count < 4 ?

 I  could  **replace  intersect  with  throughout**  if  it  were  the  latter  as  LHS  can't  be  sequence  for  throughout.

(2) In your code the local variable is incremented on posedge of clk_tb .
What if I wanted to increment it only when clk toggles and then use clk_tb for intersect operator ?


   property p_noclk_en; 
      int count=0; 
    @(posedge clk_tb) $fell(en) |=> @( clk ) (1, count=count+1)[*1:$] ##0 @(posedge clk_tb) count<4 intersect $rose(en)[->1];
    endproperty
   
     

Would this be a correct approach ?