system verilog assertion disable condition

Question

I have this assertion in order to check clk freq:

assert property clk_freq;
int cnt;
@(posedge fast_clk, clk_1MHz) disable_iff(!enable_check)
($rose(clk_1MHz), cnt=0) |=> (!$rose(clk_1MHz),cnt++) [*0:$] ##1 $rose(clk_1MHz), cnt==fast_clk_freq;
endproperty

fast_clk starts to toggle during (not from beginning) of the simulation after disable_check is asserted. The problem is that it seems that the assertion ignores the disable_iff Question: is a $rose(clk_1Mhz) event "registered" even though the assertion is disabled (or am I missing something else ?)

Answer 1

There is no disable_iff keywords, it is disable iff (without the underscore). Properties can have local variables but the local variables cannot be defined inline with assert. Separate the property definition and the assertion instantiation.

The clock sampling doesn't seem to be correct. @(posedge fast_clk, clk_1MHz) mean on rising fast_clk or any change to clk_1MHz. clk_1MHz is the sampled data value, therefore it should not be a clock.

$rose(clk_1MHz), cnt==fast_clk_freq is ilegal syntax, sugest: $rose(clk_1MHz) ##0 cnt==fast_clk_freq

Suggested property definition and the assertion instantiation:

property p_clk_freq;
int cnt;
@(posedge fast_clk) disable iff(!enable_check)
($rose(clk_1MHz), cnt=0) |=> (!$rose(clk_1MHz),cnt++)[*0:$] ##1 $rose(clk_1MHz) ##0 cnt==fast_clk_freq;
endproperty

a_clk_freq : assert property(p_clk_freq);

For more on assertions refer to section 16 of IEEE Std 1800-2012.