assertion to detect a specific switch of a signal

SystemVerilog
1

Hi all,

I have a little of experience writing properties and I got weird behavior for a property I consider quite simple…

I have a signal

typedef enum logic {
INPUT_MODE,
OUTPUT_MODE
} i2c_mode_t;

i2c_mode_t i2c_mode;

and I want to check that when this signal switches from INPUT_MODE to OUTPUT_MODE, the i2c_scl signal is 0.

The 1st version I wrote is this one below. I tried to make it has much explicit as possible in order to make it easy to read for someone unexperienced. clk_asrt is a clk of 4ns period

property i2c_switch_mode_p;
      @(clk_asrt) disable iff(sva_rst_n === 1'b0)
      ($changed(i2c_mode) && $past(i2c_mode) == INPUT_MODE && i2c_mode == OUTPUT_MODE)
      |->
      (i2c_scl === 1'b0);
    endproperty: i2c_switch_mode_p

The problem with this one is it passes once at a correct moment but never pass again while it should.

(also, when I modify the consequent into “i2c_scl === 1’b1”, the fail counter increases each time I expect him to increase)

Then I rewrote the property like that:

    property i2c_switch_mode_p;
      @(posedge clk_asrt) disable iff(sva_rst_n === 1'b0)
      (i2c_mode === INPUT_MODE) ##1 (i2c_mode === OUTPUT_MODE)
      |->
      (i2c_scl === 1'b0)
    endproperty: i2c_switch_mode_p

and this time, it works fine. The property passes each time it should.

My question is: What is different from the 2 versions ? Is there something I misunderstood with the use of $changed and/or $past ?

thank you for you help!

2

A difference I notice is in the clocking event.

In the initial property you have used clocking event as @(clk_asrt) ( which is equivalent to @(posedge clk_asrt or negedge clk_asrt) )

The latter triggers only on posedge of clk_asrt

This could be a reason to notice difference in behavior

Using the same clocking event, the 2 antecedents are equivalent

3

Thank you for your answer but this is a copy-paste error… between these 2 versions, I modified the first one to add the posedge at the @(clk_asrt). This didn’t solve the issue and behavior is still the same.

In the end, I start to think native function $past, $changed, $stable,… are a bit bugged…