How to Use Simulink Design Verifier to Automatically Detect Design Errors in Your Simulink Models

Hi, my name is Andrew, and I am a developer for the Simulink Design Verifier product at MathWorks.

In this video, I will show you how to detect design errors with the push of a button.

Simulink is a tool for Model-Based Design, and Design Verifier helps detect design errors in your Simulink models early in the development process saving time and money.

Design Verifier uses formal methods, which allows it to prove that certain design errors can never occur, and when they can, it provides a testcase that exposes the issue and helps in debugging.

First, we’ll open the Design Verifier pane on the Simulink toolstrip and run Design Verifier. For this analysis, Design Verifier will be detecting dead logic in the model. Dead logic is logic which can never be executed by the model.

Design Verifier found one instance of dead logic in this model. Design Verifier will highlight the instances of dead logic in red, which makes finding it easy. The results inspector window tells us exactly which conditions can never be exercised.

Here, tspeed < mintspeed is never true. The reason is that this transition catches that tspeed is less than mintspeed first, and then assigns mintspeed to tspeed. This means that we will never leave this state as a result of tspeed being less than mintspeed.

In actuality, we also want to transition out of this state when tspeed is equal to mintspeed, so we actually want (tspeed is less than or equal to mintspeed) to be the condition.

This is an example of where Design Verifier helps us to improve our design.

When we rerun the analysis, we now see that the model is proven to be free of dead logic.

Next, we’ll analyze the model for a run-time error, division-by-zero. Just as before, we'll press the detect design errors button, and Design Verifier will automatically perform its analysis.

In this case, Design Verifier has detected two instances of division-by-zero.

Part of the power of Design Verifier is that it will give you a testcase which can be used to help debug the error. By pressing "view test case," Design Verifier will generate a test harness for you, which you can simulate in order to debug the design error. This allows us to use all of the debugging capabilities of Simulink in order to better understand the cause of the issue.

By navigating to the errors, we can see that we are dividing by holdrate, which must be 0 in this case. This is actually a value that we have defined ourselves. The fact that we are dividing by it indicates that we don’t want this parameter to possibly take a value of 0. The fix to the error, in this case, is to change the specification of the holdrate parameter to exclude the value of 0, which is what we had intended to begin with—another instance of Design Verifier helping to improve our design!

By rerunning the analysis, we now see that the model is proven to be without division-by-zero errors.

You have now seen how to detect design errors automatically using Design Verifier. Here is the full list of design errors that Design Verifier is presently able to detect, and we’ll continue to add more in the future.

In addition to design error detection, Design Verifier is able to perform automatic test generation and prove that a model meets its specified requirements.

Thank you very much for your time, and for more information, see the links in the video description.