Counter abstraction for formal verification

In reply to ben@SystemVerilog.us:
hi Ben,
thank you for the comments.
To my understanding abstraction (of counters , memories etc.) is a general methodology and not vendor specific.
I was wondering what is the efficient way to do this?