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

SystemVerilog
1

Hello,

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?

2

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:$];

HTH
Srini