Unexpected assertion behaviour

[saw235]

Not sure if this is a bug, but I am getting failed assertion on the assert statement below, even though the counterexample waveform shows that data_wr_strobe is stable across two cycles. Which should make the assertion vacuously True, if I understand it correctly.

[piegamesde]

To help finding out more about the issue, please try to minimize the code example: strip away piece after piece while checking that the assertion fails although it shouldn't until you cannot remove any more without making it work again.

[saw235]

Hi even after I stripped down to its bare minimum, it is unclear what is happening. The following assertion below fails even though in the waveform it looks stable for 2 cycles to me.

My only guess is that the $stable() does not work like I understand it to be, or that the initial value starts off as 'X' and changes to 0 which makes the assertion fails. In the second case, I have no clue how I can get the tool to ignore time 0.

[EngRaff92]

Your clk starts as one meaning there is an active edge there, make an initial where you set the clk to 0, then in clk gen do always # clk = ~clk. To ignore time zero let the assert not be triggered by simply avoid using an evaluation point at that time. Properties has disable iff to let it be settled under reset

[saw235]

@EngRaff92 Thanks. I figured out what's wrong and managed to come up with a solution to ignore the first cycles by referencing the ibex repository.