In reply to ben@SystemVerilog.us:
I can come up with these checks:
default clocking cb @(posedge clk);
endclocking
default disable iff(!rst_n);
//Disable the assertion check for the Current count = 10000
Prop_count: assert property disable iff(!rst_n || (count[WIDTH-1] && ($countones(count) == 1)))
(1 ##1 (count == ($past(count)*2+1)));
//assertion check for the Current count = 10000
Prop_count_last: assert property count[WIDTH-1] && ($countones(count)==1) |=> (count==0));
//assertion check for termcount
Prop_ter: assert property ((count=='b0)? 1’b1 : 1’b0);