Simulink Design Verifier
Identify design errors, prove requirements compliance, and generate tests
Simulink Design Verifier™ uses formal methods to identify hidden design errors in models. It detects blocks in the model that result in integer overflow, dead logic, array access violations, and division by zero. It can formally verify that the design meets functional requirements. For each design error or requirements violation, it generates a simulation test case for debugging.
Simulink Design Verifier generates test cases for model coverage and custom objectives to extend existing requirements-based test cases. These test cases drive your model to satisfy condition, decision, modified condition/decision (MCDC), and custom coverage objectives. In addition to coverage objectives, you can specify custom test objectives to automatically generate requirements-based test cases.
Support for industry standards is available through IEC Certification Kit (for ISO 26262 and IEC 61508) and DO Qualification Kit (for DO-178 and DO-254).
Get Started:
Run-Time and Diagnostic Errors
Before you run simulations, you can detect run-time and modeling errors, including integer overflow, division by zero, array out of bounds, subnormal values, and floating-point errors as well as data validity errors.
Dead Logic
Find objects in your model that cannot be activated during simulation and execution of generated code. |
Viewing dead logic in your models.
Test Cases to Increase Coverage
Augment and extend existing manually created test cases to address incomplete model coverage. |
Requirements-Based Test Cases
Generate test cases from models of system requirements.
Test Cases for C/C++ Code
Generate test cases to increase coverage of generated code and C/C++ code called from Simulink® blocks and in Stateflow® charts.
Generating tests for models that call C code.
Safety Requirements
Verify that your design behaves according to formally defined safety requirements that you express using MATLAB®, Simulink, and Stateflow.
Simplify Models for Deployment
After you have fully validated your master variants model, use Variant Reducer to generate a reduced model for a subset of valid configurations. All related files and variable dependencies are also reduced. The reduced artifacts are packaged in a separate folder to enable easy deployment and sharing with customers and partners.
Creating a reduced model.
Detect errors for system objects
Detect errors, generate tests, or prove properties for MATLAB code using system objects in Simulink
Detect violations of High-Integrity System Modeling (HISM) guidelines
check for specific HISM violations, such as Math Function as Square Root blocks
Enable quick dead logic check
run a partial dead logic check first to debug errors found closer to design time before investing the computing time to perform an exhaustive analysis
Bus Element Support
Analyze top-level models that contain In Bus Element or Out Bus Element blocks
Improved Dead Logic Reporting
View possible causes for dead logic in the Results Inspector window, including short-circuiting and conditional execution
Parallel Test Case Validation
Use parallel computing to validate test cases or counterexamples
See the release notes for details on any of these features and corresponding functions.
