SVA disable iff not working as expected

SystemVerilog
1

I have a logic below. I want to check a is equal to b except for dis==1.

assign b = (a & ~dis);

To check this, I wrote checker as below. But as shown the attached, checker failed. I could not understand why checker failed. At posedge clk, if dis==1, I think check is disabled, but simulator says it is checked and failed. Can you please suggest what is wrong in my understanding?

   logic reset_n, clk;
   logic a, b, dis;
   bit [2:0] cnt;
   
   property chk_disiff(arg1,arg2);
      @(posedge clk) disable iff(!reset_n || dis)
        1 |-> (a==b);
   endproperty
   ast_disiff : assert property(chk_disiff(a,b));

   assign b = (a & ~dis);

   always @(posedge clk or negedge reset_n) begin
      if(! reset_n) begin
         a <= 0;
         dis <= 0;
         cnt <= 0;
      end
      else begin
         cnt <= cnt+1;
         a <= $urandom_range(0,1);
         dis <= (cnt > 5) ? 1 : 0; 
      end
   end

2024-12-27_23-27-23
2024-12-27_23-27-231428×117 2.22 KB

Thanks

2

Do not use disable iff for synchronous signals.

property chk_disiff(arg1,arg2);
      @(posedge clk) disable iff(!reset_n)
        ~dis  |-> (arg1==arg2);
endproperty
3

Hi Dave, Thank you for the suggestion. I checked some textbooks trying to understand the message, but still not sure what it really means. Can you please let me know some articles that explains in detail why synchronous signals should not be used in disable iff?
Thanks

4

You never showed is the message or gave a complete example to reproduce it.

See Within ' disable iff ( ! reset ) , is the reset synchronous OR asynchronous? - #2 by ben2