Disable iff

In some design conditions, we don’t want to proceed with the check if some condition is true. this can be achieved by using disable iff. Disable iff disables the property if the expression it is checking is active. This is normally used for reset checking and if reset is active, then property is disabled.
Below property(p) checks that, if reset is disable and the signal “a” & "b" is high on given posedge of the clock the property is asserted, During this entire sequence, if reset is detected high at any point, the checker will stop. property is deasserted.
Syntax:
property p;
@(posedge clk)
disable iff (condition);
endproperty

Example:

property p;  
@(posedge clk)  
disable iff (reset) (a&&b);  
endproperty  

The above example we use reset as the checker. The disable iff is used only inside the property. if reset is deasserted i.e '0' then the property is enabled, the assertion output is obtained. if reset is asserted then the property is disabled, then the assertion output is not obtained/displayed

code snippet

   //Design module
   module andgate(  
    input A,  
    input B,  
   output Y,  
   input clk,  
   input rst);  
  assign Y = A&&B;  
  endmodule:andgate  

//testbench

 `module AND_Gate;
 reg A;
 reg B;
 reg clk;
 wire Y;
reg rst;
//Design instantiation
andgate inst(.A(A), .B(B), .Y(Y), .clk(clk), .rst(rst));
always #5 clk = ~clk;
initial
 begin
 clk<=1;
  A<=0;
  B<=0;
  rst <=0;//assertion is enabled

  #10
 A<=0;
 B<=1;

  #10
 A<=1;
 B<=0;
 
   #10
 A<=0;
 B<=1;

  #10
 A<=1;
 B<=0;

rst <=1; // assertion is disable
  #12
 A<=1;
 B<=1;
 #100 $finish;  
  end  
 //-------------------------------------------------------  
 // Disable iff is used to disable the property when the  
 // reset is active. Assertion output is disable whether it  
 // failure or pass  
 //-------------------------------------------------------
 property p;  
 @(posedge clk) disable iff(rst) //disable if reset is assereted  
 A&&B;  
endproperty  

assert property (p) $display("%0t,A=%0b and B=%0b, assertion success\n",$time,A,B);  
else $display("%0t, A=%0b and B=%0b,assertion failure\n", $time,A,B);  

 endmodule:AND_Gate  

output:

In the below figure reset is a checker if rst=0, the property is enabled and gives the assertion output while at 40ns rst=1, the property is disabled and the assertion output is not checked. The disable iff is used when we do not want to check some output of assertion.

                                   Fig: Disable iff output

ended

The keyword "ended" is attached to the sequence name, while using more than one sequence in the program, the ending point of the sequences can be used as a synchronization point

Below in the code snippet In the property checks that, by using keyword "ended" in Ex: seq1.ended |-> ##4 seq2.ended, in this the seq1 is executed after from next clock cycle it will count for 4clock cycle,give the output of seq2 whether the condition of seq2 is fail or success. in this case the condition of seq2 is evaluated within the 4clock cycle whether it is pass of fail

code snippet

  `module assertion_ex;
   bit clk,d,k;

   always #5 clk = ~clk; //clock generation

  //generating 'a'
  initial
  begin
  d=1;
  #57  k=1;
  #10 d=0;
  #15 k=0;
  #10 d=1;
  #10 k=0;
  #10 d=1;
  #10 k=1;
  #200;
  $finish;
  end

  //sequence 1
  sequence seq_1;
  @(posedge clk)
   d;
  endsequence

 //sequence 2
 sequence seq_2;
  @(posedge clk)
  ##4 k;
  endsequence

 property p;
 @(posedge clk) seq_1.ended |-> ##4 seq_2.ended;
endproperty

a_1: assert property(p)$info("passed");
else $info("failed");

  initial
  begin
  $dumpfile("waveform.vcd");
  $dumpvars();
  end
  endmodule:assertion_ex

output:
Here, at 5ns d=1, the seq1 is executed from next cycle seq2 execute, it will check for 4cycle cycle from the ending cycle of seq1. here seq2 check the value 'k' until 45ns, at 45ns the 'k' value is low, then the assertion is failed. At 25ns the seq1 as the variable a it value is 'high', then it will start executing seq2 from next cycle, the seq2 as the variable d, it will check whether the 'k' is high with in this 4 cycle. it is high in the 4clock cycle so at 65n, the assertion is passed.

                                 Fig: Transcript output of ended

output Waveform:

                                Fig: waveform of ended

Without using ended keywordEx:seq1 |-> ##4 seq2 in this example it will execute the seq1 condition initially and then after 4 clock cycle delay it will execute the condition of seq2. Here the condition of seq2 is evaluated after 4 clock cycle

code snippet

  `module assertion_ex;
   bit clk,d,k;

   always #5 clk = ~clk; //clock generation

  //generating 'a'
  initial
  begin
  d=1;
  #57  k=1;
  #10 d=0;
  #15 k=0;
  #10 d=1;
  #10 k=0;
  #10 d=1;
  #10 k=1;
  #200;
  $finish;
  end

  //sequence 1
  sequence seq_1;
  @(posedge clk)
   d;
  endsequence

 //sequence 2
 sequence seq_2;
  @(posedge clk)
  ##4 k;
  endsequence

 property p;
 @(posedge clk) seq_1.ended |-> ##4 seq_2.ended;
endproperty

a_1: assert property(p)$info("passed");
else $info("failed");

  initial
  begin
  $dumpfile("waveform.vcd");
  $dumpvars();
  end
  endmodule:assertion_ex

output:
Here, at 45ns d=1, the seq1 as variable 'd' it is high at 45ns, then seq1 is executed, then now seq2 will start execute the variable 'k' after the 4clock cycle, it will start to check the value of 'k',after the 4clock cycle of seq2, then seq2 variable 'k' is execute after the 4clock clock. total it take 8clock cycle to execute the seq2 value, at 125ns it will pass the assertion.

                           Fig: output of without_ended

output waveform:

                              Fig: output waveform of without_ended