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