Simulink Design Verifier uses formal methods to identify hidden design errors in models. It detects operations in models that result in run-time errors and undesired behaviors, such as integer overflow, dead logic, array access violations, and division by zero. The analysis is distributed across CPU cores to accelerate results for complex models.
Simulink Design Verifier performs formal verification to prove that designs meet functional requirements and do not violate safety requirements. Formal analysis also verifies requirements for consistency and completeness. For each design error or requirement violation, the software generates a simulation test case for debugging.
Using Simulink Design Verifier, you can automatically generate test vectors to achieve model and code coverage. These test vectors drive your model to achieve decision, condition, and modified condition/decision (MC/DC) coverage metrics.
Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178 and DO-254).
Validate Requirements
Check modeled requirements for consistency and completeness before implementing your design.
Detect Run-Time and Diagnostic Errors
Before running simulations, you can detect potential run-time errors and modeling issues, including integer overflow, division by zero, and array out of bounds errors; subnormal values and other floating-point errors; and data validity errors. Use Defect Checker for quick, targeted, and interactive error checking.
Find Dead Logic
Find model logic that cannot be activated during simulation and execution of generated code. Such logic cannot be tested and often indicates a logical error. Review analysis results and trace likely root causes to remove this dead logic before implementation.
Analyze Missing Test Coverage
Automatically generate test vectors to augment and extend existing manually created test cases. Use the extended test cases to address incomplete model coverage and incomplete coverage of C/C++ code called from Simulink blocks and Stateflow charts.
Verify Formal Safety Requirements
Verify that your design behaves according to formally defined safety requirements that you express using MATLAB, Simulink, and Stateflow.
Create Requirements-Based Test Cases
Generate test cases from models of system requirements.
Perform Back-to-Back Testing
Compare model simulation results with results from SIL or PIL simulations based on generated code to verify equivalence or reveal discrepancies before deployment.
Generate Code Coverage Tests
Generate test vectors to exercise generated C/C++ code, then review coverage results to identify gaps that model coverage alone may not reveal.
Product Resources:
“By enabling us to analyze requirements quickly, reuse designs from previous products, and eliminate manual coding errors, Model-Based Design has reduced development times and enabled us to shorten schedules to meet the needs of our customers.”
Simulink Design Verifier FAQs
Simulink Design Verifier uses formal methods to identify hidden design errors in models, verify that designs meet functional requirements, and generate test cases for model coverage and custom objectives.
It detects model elements that result in integer overflow, dead logic, array access violations, division by zero, subnormal values, floating-point errors, and data validity errors.
Dead logic refers to logic in your model that cannot be activated during simulation or execution of generated code. Because this logic can never execute, it cannot be tested and may indicate a design or implementation error. Simulink Design Verifier uses formal analysis to identify this inactive logic and help you detect potential issues early in development.
It automatically generates test cases to satisfy condition, decision, modified condition/decision (MCDC), and custom coverage objectives. It can also generate requirements-based test cases from models of system requirements.
Yes, it can verify that your design behaves according to formally defined safety requirements expressed using MATLAB, Simulink, and Stateflow, and it generates a simulation test case for each design error or requirements violation for debugging.
Yes, 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.
It analyzes missing test coverage and augments existing manually created test cases to address incomplete model coverage and incomplete coverage of generated C/C++ code called from Simulink blocks and in Stateflow charts.
Yes, it can check modeled requirements using the Requirements Table block for consistency and completeness before you begin implementing your design.
Try Simulink Design Verifier for Free
Discover the possibilities today.
Ready to Buy?
Get pricing information and explore related products.
Are You a Student?
Your school may already provide access to MATLAB, Simulink, and add-on products through a campus-wide license.
