MATLAB Answers

Falsified - No counterexample in Simulink Design Verifier

조회 수: 1(최근 30일)
Yvonne Murray
Yvonne Murray 2020년 11월 29일
답변: Aman Vyas 2020년 12월 16일
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, 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?


Aman Vyas
Aman Vyas 2020년 12월 16일
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 !

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by