The assertion is active although the signal hasn't changed from high to low

SystemVerilog
, ,
1

My assertion is active at the first i_adc_start even though o_c_15k6 is low (not changed from high to low). I understand the assertion treats it as a change at the first i_adc_start (May be it treats that it’s changed from x-0). How to avoid this

property acs_c_15k6_toggle_check_high_5c;
int v;
@(posedge i_adc_start) disable iff(i_en || i_start_seq)

$rose(o_c_15k6) |->if(i_c_15k6_freq == 2'b00) o_c_15k6[*8]
                   else if(i_c_15k6_freq == 2'b01) o_c_15k6[*16]
                   else if(i_c_15k6_freq == 2'b10) o_c_15k6[*32]
                   else if(i_c_15k6_freq == 2'b11) o_c_15k6[*64];
endproperty
2

In reply to Nandeesha:

My assertion is active at the first i_adc_start even though o_c_15k6 is low (not changed from high to low). I understand the assertion treats it as a change at the first i_adc_start (May be it treats that it’s changed from x-0). How to avoid this
property acs_c_15k6_toggle_check_high_5c;
int v;
@(posedge i_adc_start) disable iff(i_en || i_start_seq)
$rose(o_c_15k6) |->if(i_c_15k6_freq == 2’b00) o_c_15k6[*8]
else if(i_c_15k6_freq == 2’b01) o_c_15k6[*16]
else if(i_c_15k6_freq == 2’b10) o_c_15k6[*32]
else if(i_c_15k6_freq == 2’b11) o_c_15k6[*64];
endproperty

Although I have disabled when reset is low and used !$isunknown(o_c_3k9). It’s still the same

@(posedge i_adc_start) disable iff(i_en|| !i_rst_n )
//($rose(o_c_15k6), v=clk_count_c_15k6)|-> (o_c_15k6 throughout (v>=0, v=v-1)[*0:$]) ##1 !o_c_15k6;
(!$isunknown(o_c_3k9) && $fell(o_c_3k9)) |->if(i_c_3k9_freq == 2'b00) !o_c_3k9[*32]
                   else if(i_c_3k9_freq == 2'b01) !o_c_3k9[*64]
                   else if(i_c_3k9_freq == 2'b10) !o_c_3k9[*128]
                   else if(i_c_3k9_freq == 2'b11) !o_c_3k9[*256];
endproperty
3

In reply to Nandeesha:

Please use code tags making your code easier to read. I have added them for you.

From your previous questions, are you sure you mean to have i_adc_start as the clock?

4

In reply to dave_59:

Sorry for the delayed response. Yes, I need to count the i_adc_start signal to check the stability of o_c_3k9 signal.

5

In reply to Nandeesha:

How about creating a small runnable example?