Avoid first_match operator

[ajeethakv]

The first_match operator in SVA triggers a property once after the initial state. To determine if a match never occurs, the design may need unrolling to its full sequential depth, potentially causing state space explosion. This makes the problem size dependent on the design and possibly proportional to its total number of states. Due to these challenges and the complexity it introduces in formal verification, the first_match operator is often excluded from the supported subset in formal verification tools.

[ajeethakv]

https://agra.informatik.uni-bremen.de/doc/konf/08_dsd_svachecking.pdf