Guiding the proof?

Hello!

Let’s say I want to prove an assertion:
property p is always { cond_a : seq_s } |-> cond_b;
assert p; – Inconclusive after many hours

I can however prove:
property p1 is always cond_a → cond_c;
property p2 is always { cond_c : seq_s } |-> cond_b;
assert p1; - Takes few seconds
assert p2; - Takes few seconds

If I now change p1 and p2 into assumptions I can successfully prove p:
assume p1;
assume p2;
assert p; – Conclusively proven in few seconds

Is there a way to do that automatically in PropCheck?

Thanks,
DK
PS: Apologies for using VHDL syntax in SV forum

In reply to Delta Kilo:

This Mentor/Siemens EDA sponsored public forum is not for discussing tool specific usage or issues. Please read your tool’s user manual or contact your tool vendor directly for support.

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

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.

In reply to Delta Kilo:

Hi DK,
PropCheck tools may have automatic assume-guarantee feature, i.e., automatically use proven assert properties as assumptions for proving other inconclusive assertions. For your example, if you add p, p1 and p2 in the same run, some tools can use p1 and p2 as assumptions for proving p if it can prove p1 and p2 before proving p. Please contact your tool vendor to know the detail.