$rose & $fell
In SVA we can write:
-
$rose(a)
to mean "a
is now1
, but it was0
in the previous step (if that step exists)". -
$fell(a)
to mean "a
is now0
, but it was1
in the previous step (if that step exists)". -
$stable(a)
to mean "a
has 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 !a
.
Note: SVA can also combine these notations with clocks, and in this case looking one step back is not enough.