Avoid unbounded repetition - continuous

[ajeethakv]

The [*1 : $] operator represents a sequence that repeats at least once but has no specified upper limit. To verify if all design traces match or don't match this sequence, the design may need to be unrolled up to its sequential depth. This unrolling process can significantly increase the problem size, potentially making it proportional to the total number of design states. Due to this complexity, the [*1 : $] operator is often not supported in formal verification tools. Instead, sequences are typically constrained to a bounded number of time steps, ensuring more manageable verification processes.