In reply to Delta Kilo:
Hi DK,
As Dave mentioned, contact your vendor for some more specific questions related to formal tools.
Generally speaking with formal, proven properties can help prove properties that are still running.
There is the concept of helper assertions, which are simpler assertions, typically invariants, which can be used to help prove more complex properties.
The method you used above is valid with formal. One term for it is decomposition, where a complex property is decomposed into its simpler elements, these can then be more easily proved and once these are proven, the original property is typically proven.
When writing properties for formal you typically want to keep them simple and sequentially short. In the above property if you have a long sequence in the antecedent, the formal engine may not get to a depth such that the property may be fully evaluated.
With formal, it is all about state space and minimizing that to get a result. You can think of it from the terms that every cycle of evaluation you do into the design you are doubling the size of the problem. It is a geometric curve. The downside is that there is a limitation as to the depth of analysis you can perform, the benefit is for the give property you have explored every scenario. That is why formal finds corner case bugs that are often missed in simulation. In your planning it may make sense to run certain properties in simulation and others in formal. That is design and function specific of course.
I won’t go into more detail on this as this is a language and methodology forum. Short answer is the method you have used above is certainly a valid one when using formal and dealing with inconclusive properties.