Hey,
I just had a huge performance issue in my simulation, I was able to narrow it down to a single assertion that made the issue.
I had no idea that an assertion could cause performance issues.
This is the assertion:
@(posedge clk) ##[0:$] x[->2];
Would be great if someone can explain why it slowed my simulation so much.
In reply to nnn314:
Hello could you explain what are you trying to check maybe there could be multiple way to define the same checker.
Anyway in your case you experiencing an overlap issue since no enabling condition is set. Each evaluation point a new check will be spawn causing probably the simulation to be overly slowed down. Maybe if you could explain more in depth what are the specifications you are trying to check we could create a disable iff condition or an enabling condition.
Regards
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
In reply to nnn314:
Yes exactly so seems like every evaluation point a new thread is spawn waiting for the fulfilling condition to be verified. That is the reason why by reducing the time you check the property then you experienced a profomance improvement compared to the first time. Probably if you run formal with just that property being checked i would guess you will see the resources kind of reaching the limit you set almost after fee cycles due to the amount of threads spawned waiting to be true.
Someone who knows formal tool more in depth then me could comment better on it.