Working of disable iff

SystemVerilog
, ,
1

Hi All,
For the following example ::

  bit clk , a , b , dis ;
  
  always #5 clk = !clk;
  
  initial begin
  `ifdef NBA 
    #05; dis <= 1;  // T:5 overlaps with posedge of clock
    #10; dis <= 0;
    #05; dis <= 1;  // T:20
    #10; dis <= 0;  // T:30
  `else
    #05; dis = 1;   // T:5 overlaps with posedge of clock
    #10; dis = 0;
    #05; dis = 1;   // T:20
    #10; dis = 0;   // T:30
  `endif   
  end  
  
  assert property( @(posedge clk) disable iff(dis) a == b  ) $display("T:%0t Pass",$time); 
                                                        else $display("T:%0t Fails",$time);
    
 initial begin
   #04; a = 1 ; b = 1; 
   #10; a = 0 ; b = 1; 
   #10; a = 1 ; b = 0; 
   #10; a = 1 ; b = 1; 
   #2; $finish(); 
 end

At time:5 units there is posedge of clock as well as dis is assigned 1 (either in NBA or active region)
At time:15 units there is posedge of clock as well as dis is assigned 0 (either in NBA or active region)

I am aware that the expression within disable iff is asynchronously checked,

(1) So when dis is 1 at T:5 , will the assertion be disabled OR would it evaluate ( a == b ) ?

(2) So when dis is 0 at T:15 , will the assertion be active / re-enabled and evaluate ( a == b ) ?

2

See discussion at

3

Also see

4

Thanks Ben.
Via both (1) & (2) assignment to ‘dis’ is done before the observed region starts at T:5 & T:15.
Hence the assertion attempt is disabled at T:5 ( as ‘dis’ is 1 ) whereas evaluation takes place at T:15 ( as ‘dis’ is 0 )

5

I also tried examples with the expression within disable iff being true in ::
(a) observed region ( edalink )
(b) reactive region ( edalink using +define+REACTIVE )

For (a) at 1st attempt at T:5 the expression is true in observed region,
hence the SVA is active at T:5.
There are no attempts at following posedge of clock at T:15 , 25 ,35 as the disable iff expression is true

For (b) during the 2nd attempt at T:15 the expression is true in reactive region,
hence the SVA is active at T:15.
There are no attempts at following posedge of clock at T: 25 ,35 as the disable iff expression is true