How to write SVA assumption

In reply to ben@SystemVerilog.us:

In reply to dplumb_amd:
The assume assertion looks OK. What is wrong? the formal?

Yes. Formal is generating a counter example that seems to be violating my constraint.