Stable pwrite until pready

SystemVerilog
1

I was curious to understand this semantic here I’ve seen in a public repo:

The requirement:

pwrite remains stable (unchanged) throughout the entire wait state period of an APB transaction — from when penable rises until pready asserts.

The property:

property p_stable_pwrite;
  disable iff(!presetn) 
  $rose(penable) ##0 !pready[1:$] |-> $stable(pwrite);
endproperty

Can we say the antecedent is a multicycle sequence that lasts from when penable raises and pready remains low? I have hard time picturing it.

IMHO the antecedent is not a multicycle of the usage of $rose which will not be true on the second cycle and therefore the behavior of pwrite will only be checked for the first cycle.

A more appropriate check would rather be something along these lines:

property p_stable_pwrite;
  disable iff(!presetn) 
  $rose(penable) |->  !stable(pwrite) throughout pready[->1];
endproperty

Thanks for your comments

EDIT: additional analysis and a proposed alternative