Design Verifier compatibility with SimEvents blocks

Is it possible to use property proving in the Design Verifier toolbox with a model using SimEvents blocks? I have tried to add a simple verification property within a verification subsystem to an example SimEvents model, but when I try to run the property prover I get the following error: "Building model representation failed: Simulink Messages blocks support only Normal mode simulation."

I did not alter the example model at all, except for adding a verification subsystem:

Inside the verification subsystem, I added a simple property to prove that the number of rejected parts is less than 10:

Answer 1

[Abdolkarim Mohammadi]

I haven't used Design verifier with SimEvents blocks, but I think the error message is clear. The model containing SimEvents blocks and Design verifier blocks must be run only in Normal mode, not Accelerated or other modes.

[Nathan Puryear]

Thank you for the reply, but I disagree that the error message is clear. It would seem that it is clear, except that the simulation mode is in "Normal" mode. I have searched online to see if there is anything specific to design verifier's configuration regarding the simulation mode, but I have found nothing.

I have not changed any of the standard configurations from the provided example model, and I have verified that the simulation is set to "Normal."

[Pat Canny]

Hi Nathan,

Thanks for your question. This is an interesting use case.

I tried running that example, but noticed that it uses a variable-step solver, which is not supported by Design Verifier.

Did you change the solver to fixed-step before running into the Normal mode error? The solver incompatibility should have popped up first...

[Nathan Puryear]

Hi Pat,

Yes, I did set the model to use a fixed-step solver; I forgot to mention that. If you set the model to use a fixed-step solver, and try to prove properties using Design Verifier, do you see the same error message that I have in the original post?

Thank you,

Nathan

[Pat Canny]

Hi Nathan,

When doing so using R2020b, I get the same error.

In R2021a, I got a different error (which is probably the actual problem). This model includes elements which do not generate code. When Design Verifier checks for compatibility, it "translates" the model into an intermediate representation using similar technology to the code generation engine. Anything in the model that does not generate code would (in general) be incompatible. I do not know why this error wasn't reported in R2020b. I have passed this along to our software development team.

I have to ask, though (not being as familiar with SimEvents) - is changing the solver setting going to result in different behavior? I saw that the model simulates, but are the results the same with a fixed-step solver?

[Nathan Puryear]

Pat,

So, based on the code generation capabilities, Design Verifier is not compatible with SimEvents blocks? If that is the case, then I think this is solved.

As far as I can tell, changing the solver setting doesn't result in different simulation behavior for the example model.

Thanks,

Nathan

[Pat Canny]

Hi Nathan,

In general, yes: Simulink Design Verifier is not compatible with SimEvents blocks. Apologies again for the confusing error message.

Thanks.