Falsified - No counterexample in Simulink Design Verifier

When I am in property proving mode, and use the strategy "FindViolation", I get the result "Falsified - no counterexample" (this takes about 3-4 seconds). In the list of objective statuses at https://ww2.mathworks.cn/help/sldv/ug/simulink-design-verifier-reports.html#bq9oel8, I can't even find the option of falsified without counterexample.

When I use the strategy "Prove" it times out after my limit of 8 hours, without getting a result. Thus, I have no counterexample, and I am wondering what to make of the results. Can I assume that the property is really falsified? Then shouldn't it be able to provide a counterexample if that's really the case? Would extending the time for the "Prove" strategy help, or is it sometimes the case that it does not reach a conclusion?

Answer 1

[Aman Vyas]

Hi,

Mostly the formal verification methodology tends to give counter example whenever the eqivalence is not matched.

But if it giving out falsified option and not able to generate the counter-example corresponding to it then the design must have been very unique or tool might not be able to produce the example. This will require looking into the model first.

On contrary , you can Try clicking on "Create harness model" in the Results window and running the simulation.

The objectives will no longer be falsified only when the design error in the model is fixed.

Hope it helps !