Regarding disable iff

SystemVerilog
, , , , ,
1

Hi Dave/Ben,

[1] Section 16.9.3 of the LRM mentions

The use of $sampled in a disable iff clause is meaningful since the disable condition by default is not sampled (see 16.12).

Section 16.12 further mentions

The disable condition is tested independently for different evaluation attempts of the property_spec.
The values of variables used in the disable condition are those in the current simulation cycle, i.e., not sampled.

[Q1] I am not clear on the above 3 lines.

I am aware of the following ::
(a) Expression within disable iff is evaluated asynchronous to the clocking event and when found true the evaluation is disabled i.e no property_expr evaluation, no action block execution.
(b) $sampled returns the pre-poned value of it’s argument.

[2] Syntax 16-16 of the LRM mentions

property_declaration ::=
property property_identifier [ ( [ property_port_list ] )  ] ;
{ assertion_variable_declaration }
 property_spec [ ;  ]
endproperty [ :  property_identifier ]

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

[Q2] Doesn’t this imply that the clocking event ( when explicitly specified ) should precede the disable iff clause ?

Surprisingly both of the following work

sva1:assert property( @(posedge clk) disable iff(!rst_n)  property_expr1 );
sva2:assert property( disable iff(!rst_n) @(posedge clk)  property_expr1 );

I expected sva2 to throw a compilation error due to the compiler enforcing clocking_event should precede disable iff ( expression_or_dist )

Thanks in advance

2

[Q2] Doesn’t this imply that the clocking event ( when explicitly specified ) should precede the disable iff clause ?
[Ben] It does seem so. However, in the property_spec the following are optional:
[clocking_event ] [ disable iff ( expression_or_dist ) ]
Thus, I could write:

property p;   @(posedge clk) a;  endproperty // legal 
// Also legal
sva3:  assert property (disable iff (rst_n) p);
// Now if I expand "p", SVA3 becomes
sva3:  assert property (disable iff (rst_n) @(posedge clk) a;
// THUS, going back to your Q: 
sva1:assert property( @(posedge clk) disable iff(!rst_n)  a );
// sva1 is per the definition nof the 
property_spec ::=
[clocking_event ] [ disable iff ( expression_or_dist )  ] property_expr
// sva2 is like my sva3 where property "p" is the (@(posedge clk)  a) and the clocking event  is optional. 
 sva2:assert property( disable iff(!rst_n) @(posedge clk)  a );

https://www.edaplayground.com/x/EF2a
All vendors compile and simulate the code 

Q1 answer tomorrow
3

On the disable iff:
From my new book:
• Asynchronous disable iff: Uses an expression (e.g., 0 for no disable) or a module variable (e.g., reset). The variable’s value is NOT sampled and represents the value in the Observed region when the assertion is evaluated.
• Synchronous disable iff: Two common techniques for synchronous reset implementation:
o Explicit clock specification

     disable iff  ($fell(reset_n, @(posedge clk)))  // /ch3/3.8/reset2.sv
    // disable sampled at @ (posedge clk)

o $sampled function: Sampling occurs in the time stamp that the assertion is evaluated.
The time stamp is the event that triggered the assertion.

            		disable iff  ( $sampled(!reset_n)) // resets when the sampled value of reset_n==0

More questions?
“Fast-Tracking SVA through Exposure”
AMZN Paper copy: LinkedIn
PDF: Fast-Tracking SVA through Exposure: Core Usage, Concepts, AI Integration - Payhip

4

Q2 - I would argue (agree with OP) that it seems illegal as per LRM (or atleast ambiguous). FWIW, Verible parser does fail on such usage.