In reply to ben@SystemVerilog.us:
Hi Ben
Thank you for the explanation and solution. I have one question in the solution. For property which is working, I think we donot need local variables in the property. I have made some modifications below. Please let me know your views.
property p_countab_ok;
//int va=0, vb=0;
(go, do_calc(0, 0, go, done)) |->
(##[1:$] (a || b, do_calc(a, b, go, done)) ##0 done) or
(done[->1], do_calc(0, 0, 0, done));
endproperty
ap_countab_ok: assert property(p_countab_ok);