Why does this assertion behave like this?

Hi everyone!

I'm currently watching the lessons for the "SystemVerilog Assertions" course, and while doing the lab exercises I incurred in a behaviour which I can not understand. In lab 4, which requires to work on a SPI-like communication module, I need to cover a specific case in which the transaction's header (i.e. the first 8 bits of the transactions, which arrive LSB first starting from the clock cycle after the one in which the "frame" signal is asserted) does not correspond to any known sequence. Let's assume I write my code like this (not exactly what the lab asks for, but this way it's simpler to explain my issue):

localparam cfg = 8'b11001101;

...

sequence check_header(header);
     int i = 0;

    (serial == header[i], i++) [*8];
endsequence

...

cvg_ukn: assert property ( @(posedge clk iff !suspend) (
             $rose(frame) |=> not(check_header(cfg))
      )
);

What happens when I simulate is that the assertion becomes active when frame's rising is detected (the design is edge-negative, so the assertion detects it on the next rising clock edge), but then in the next cycle it becomes inactive! I do not understand: why does it become inactive? Is there something in the meaning of my consequent that I do not understand? Is there some tool configuration conflicting with what I wrote?

I now that the same property can be written in other ways (I know how to do that too), but I would really like to understand what's going on here.


(As side information, I'm working on Xcelium 21.03 and I run it with the command "xrun -64bit -SV -gui -access +rwc -svseed 1 -linedebug -abvrecordcoverall -input nc_input.tcl
spi.sv spi_test.sv top.sv" provided as a default script together with the labs files)



EDIT: I tried a run with QuestaSim and the assertion works, so I'm starting to think it must be something related to Xcelium...