Assertion fails when signal value transitions from X to stable state

SystemVerilog
,
1

I am trying to write an assertion (my very first one) that checks if the value of an enum is within a defined set when the valid signal is high. This is what I have:

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

This mostly works fine but it fails when the value of state_e enum was ‘X’ before the clock edge and I am not sure why!

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.”

3

In reply to dave_59:

Thanks, that makes it clear! :)