Assertion fails when signal value transitions from X to stable state

SystemVerilog
,
2

In reply to 90qtq2tjgqp0tg78:

Assertions use sampled values, which are the values they have immediately before the clock edge. But the disable iff expression is asynchronous. What you probably meant to write is

 assert 
    property(
      @(posedge clk) disable iff(!arst_n)
  valid |-> state_e inside {S1, S2, S3}
    );

This says: “when the sampled value of valid is high, state_e must be inside the defined set, otherwise when valid is low, we don’t care.”