Hello,
I would like to know if there are any benefits (especially performance wise) of using the $future_gclk based operators (the ones that look into the very next clock cycle) over $past based ones.
I understand that it might be easier for formulate some properties in some scenarios, but what I really care about is if the use of some might be the factor that decides if a check converges or not.
I would be happy to hear your explanation.
If you have any sources or material that I could explore, I would also gladly do so.
Best