In reply to ben@SystemVerilog.us:
An option for your 1st property using the Non-consecutive repetition, Boolean([=n]
property p_lock_condition_check_unlock_prog_00_Voption; // Using |-> ##1 (consequent)
//int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00) |->
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:6])
##0 o_fll_lock;
endproperty