$rose & $fell
In SVA we can write:
$rose(a)to mean "
1, but it was
0in the previous step (if that step exists)".
$fell(a)to mean "
0, but it was
1in the previous step (if that step exists)".
$stable(a)to mean "
ahas the same value in the previous step if that step exists"
If we had past operators, we would be able to write the first one
a & (Y(!a) | !Y(1)) and the other two similarly. But even without past operators, these seem to be something we could translate quite easily because they are only looking one step back.
For instance if during a translation one state is labeled by
$rose(a) we know that all outgoing transitions match
a, and all incoming transitions match
Note: SVA can also combine these notations with clocks, and in this case looking one step back is not enough.