In reply to Tudor Timi:
In reply to ben@SystemVerilog.us:
I don’t get what you mean by “no default disable iff”. W.r.t. $rose(rst_n), I’m still mulling it over. During reset, the circuit is anyway in a coma. What you care about is what values you get when coming out of reset. Even (some of) the ARM specifications specify behavior like this, e.g. what value HREADY has when coming out of reset.
One thing I noticed we were both missing is a check for “no count without count enable”.
[Prabhu] Yes, it’s missing
The assert property for same
ap_nocount_wo_cen: assert property(##1 !ld_enb && !count_enb && count_out!=0 |=> $stable(count_out));
(or)
ap_nocount_wo_cen: assert property(##1 !ld_enb && !count_enb && count_out!=0 |=> count_out==$past(count_out) );