Simulink Design verifier does not terminate.

Hi,

i have an issue with the simulink design verifier toolbox. I'm trying to do a formal verification of my model, by comparing the outputs with another model, of which that it works 100% correct. I use the property proving mode. The outputs of these to models must be the same for a successful verification. The backround is, that i try to verify an algorithm, which i developed.

No my problem is, that the process does not terminate. It ran up to 13 hours without any decision. Can anybody help me? Is there a possibility to debug during verifier execution? Did anybody have this issue too?

Thanks

Mirhad

PS: I'm using R2022a. I already tried with R2022b, but it didn't help.

Answer 1

[Pat Canny]

Hi @Mirhad,

My first suggestion is to consult this item in our documentation: Prove Properties in Large Models.

It looks like you might be following a similar workflow to my recently created Formal Equivalence example - is that so?

One suggestion (which is also included in the documentation above) is to try using the 'FindViolation' strategy first (as I did in the example).

Some simple code to demonstrate:

opts = sldvoptions;
opts.Mode = 'PropertyProving';
opts.ProvingStrategy = 'FindViolation';
opts.MaxViolationSteps = 99;

'FindViolation' (as opposed to 'Prove') often tends to take less time to run.

How large are the models being analyzed? How many objectives are being analyzed? (Is it just one Proof Objective?)

You can stop analysis and generate results for debugging, however you'd only be able to analyze results for completed objectives.

If you continue to run into long analysis times, I recommend reaching out to MathWorks Technical Support.

[Mirhad]

Hi,

thanks for your answer. I found the reason. I used a 32-bit unsigned integer as counter to detect changes an the design verifier tried to provoke a overflow. Saturating the counter fixed this issue.