About concurrent assertion in FSM

Implication operators can only be used inside property expressions. Where you’re using it, it is inside a sequence expression, hence the syntax error.

Can’t help you rewrite that though, as you didn’t describe what the property is supposed to do, and I can’t make it out from your code.