In reply to dave_59:
Hi Dave, thanks for answering. I suppose I asked the wrong question. The right question is:
How do I express the relationship “Properties P1,P2 need to first formally proven then assumed in order to formally prove property P” in SVA or PSL or any other assertion language?
In my case property P is simple, high-level and general. The substitution cond_a → cond_c is far from trivial and I do not expect the tool (any tool) to stumble on it by accident or to deduce it by itself without a guidance.
If I can’t express this in the language (which I suspect is the case), the next best thing is to see if a tool can provide these options, maybe I can manually specify the order in which assertions are to be proven or if there are dependencies between them. Failing all that I can resort to some hackery like having running the proof in multiple passes and have pass number specified by a generic parameter.
BTW we are evaluating formal verification at the moment and haven’t settled yet on the language or toolset. From what I see I’m starting to have doubts about the whole thing. As I understand it, there is no guarantee whatsoever that the tool can actually prove any property assertion in finite time, even “assert 2*2=4”, all I can hope for is “best efforts”. I’ve seen situations where adding extra assumptions would cause the proof to break down and timeout after many hours where it completed successfully in a few seconds before the assumptions were added. This is the kind of scenario where I may need to guide the proof manually to get it to complete.
Regards,
DK