Write sva assumption for signal to be specific value at specific time


I have a question about SVA assumption:
If I have STAR signal, I want it to be 1 at the first clock cycle and 0 for the entire time. In the assume statement we cannot use sequences. How can we do that?

You can use assume with seq/property (Unless a tool restricts so). Now, detecting “first clock” is tricky, but second part of your Q is sort of easy:

$fell(STAR) |=> !STAR[*1:$];