How to write SVA assumption

SystemVerilog
2

In reply to dplumb_amd:

The assume assertion looks OK. What is wrong? the formal?