Falsified - No counterexample in Simulink Design Verifier

조회 수: 4 (최근 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 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?

답변 (1개)

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 !


Help CenterFile Exchange에서 Address Model Incompatibilities or Analysis Timeout에 대해 자세히 알아보기

Community Treasure Hunt

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

Start Hunting!

Translated by