Questions on disable iff

SystemVerilog
, ,
1

Hi All,
Consider the following 2 concurrent assertions ::

module top_tb ;  
  bit clk , a , b , dis ;  
  always #5 clk = !clk;

  initial begin
    #05; dis = 1;
    #10; dis = 0;  // T:15
    #05; dis = 1;  // T:20
    #10; dis = 0;  // T:35
  end  
  
  ap1:assert property( @(posedge clk) disable iff(dis) a == b ) $display("T:%0t ap1 Pass",$time); else $display("T:%0t ap1 Fails",$time);
    
  ap2:assert property( disable iff(dis) @(posedge clk) a == b ) $display("T:%0t ap2 Pass",$time); else $display("T:%0t ap2 Fails",$time);    

  initial begin
   #04; a = 1 ; b = 1; 
   #10; a = 0 ; b = 1; 
   #10; a = 1 ; b = 0; 
   #10; a = 1 ; b = 1; 
   #02;$finish();  
  end         
endmodule

LRM Syntax 16-16—Property construct syntax mentions ::

property_spec ::=
[clocking_event ] [ disable iff ( expression_or_dist )  ] property_expr

Note that ‘disable iff’ comes after the clocking event.
However when tested on EDA tools both the concurrent assertions ‘ap1’ and ‘ap2’ compile and simulate.

[Q1] Shouldn’t ‘ap2’ throw a compilation error ?

[Q2] What does ‘dist’ in ‘expression_or_dist’ mean ? The only place where I have personally used ‘dist’ is during randomization for distribution weights

2

Those are very nice questions :)

[Q1] I don’t think it should. So, as mentioned in 1.6 Syntactic description "The formal syntax of SystemVerilog is described using Backus-Naur Form (BNF)" and also "Square brackets ( [ ] ) that are not in boldface-red enclose optional items."
That means [clocking_event ] [disable iff ( expression_or_dist )] are
optional items and the parser should be able to handle all their possible combinations of existence, and about whether the order in which optional items are defined will matter or not that should be mentioned in the language grammar. I checked [Annex A (normative) Formal syntax, Annex F (normative) Formal semantics of concurrent assertions], and I couldn’t find anything explicitly saying that the order matters. I guess that will leave it open to the implementer.

[Q2] dist could be also used but it’s only meaninful in case of assume directive, with assert it’s equivalent to inside as mentioned in 16.14.2 Assume statement "The biasing feature is useful when properties are considered as assumptions to drive random simulation. When a property with biasing is used within an assert or cover assertion statement, the dist operator is equivalent to inside operator, and the weight specification is ignored"

Personally, I haven’t used it in a disable iff within a simulation context, but I can see it could be useful in a formal setup. I’ve created the following example, and it seems to be working as expected
[caveat: only one EDA provider supports it so far on EDAplayground]

EDA_link

module top_tb ;  
  bit clk , a , b;
  bit[1:0] dis;
  
  always #1 clk = !clk;
	
  asrt_0 :assert property( @(posedge clk) disable iff(dis dist {0 := 10, 1:= 20}) a == b ) $display("T:%0t asrt_0 Pass",$time); else $display("T:%0t asrt_0 Fails",$time);
      
  initial begin
   #0 dis = 2;
   #1 a = 0 ; b = 1; 
   #3 dis = 0;
   #5 dis = 2;
   #5 dis = 1;
  end
    
  initial begin
    $dumpfile("dump.vcd"); $dumpvars;
  	#25 $finish();   
  end
endmodule

P.S. All my conclusions are based on IEEE Std 1800™-2017