In reply to Rsignori92:
Hey Rsignori92,
First of all thanks for your answer!
The property is supposed to catch an occurrence of a signal twice, non-consecutively/consecutively, during the time of simulation.
The property is aimed to be a cover property for the time I run a specific scenario that creates this signal twice (Error injection).
I did manage to solve the issue by changing the property to:
@(posedge clk) x[->2] within (counter > 0 && counter < SOME_PARAMETER)
I still haven’t verified that it is doing what I specified above, but it solved the performance issue.
What was important for me is to understand why it happened in the first place.
So when you say “Anyway in your case you experiencing an overlap issue since no enabling condition is set” you mean that there is nothing to be evaluated at the LHS?
Thanks in advance