SVA for FSM

In reply to nimitz_class:

I’m guessing you have not stated your requirements properly, so please explain why this would not work:

property ladder_values_check (rclk, fsm, ladder_value) ;
  @(posedge rclk) (fsm == S1 || fsm == S7) |-> ladder_value == 8'h90;
endproperty