SVA: condition met between two disabled sections not showing pass/finish

SystemVerilog
,
17

In reply to Adarsh Santhosh:
Yes on “As per my understanding, any change in signal should act as trigger. can the signal be multibit?”

But if TN.state wil introduce other issues in the assertion. For example:


module m;
  bit[3:0] a; 
  bit clk, b, c; 
  initial forever #5 clk=!clk; 
  always @(posedge clk) begin 
    a <= 1+1; b <= !b; c<=a[2]; 
  end
  
  ap_1: assert property(@(a) b|-> c);
    
    initial begin 
    #100; 
    $finish;
  end 
endmodule

Here, in ap_1, the sampled value of b is not the one preceding the posedge of clk (in the preponed region). That’s because a changes in the NBA region, which is also where all the b and c also changes; the order of changes is not guaranteed.
You are asking for trouble.