Simulink Design Verifier
Simulink Design Verifier applies formal methods to uncover hidden design issues in models. It identifies problematic blocks that can cause integer overflows, dead logic, array access violations, or division by zero. It also performs formal verification to confirm that your design satisfies functional requirements. For each detected design error or requirement violation, it automatically generates simulation test cases to support debugging.
The tool also generates test cases to enhance model coverage and meet custom objectives, complementing existing requirements-based tests. These cases exercise your model to achieve condition, decision, modified condition/decision coverage (MCDC), and user-defined coverage goals. You can also define custom test objectives to automatically generate additional requirements-based test cases.
Support for industry standards is provided through the IEC Certification Kit (for ISO 26262 and IEC 61508) and the DO Qualification Kit (for DO-178 and DO-254).
Validate Requirements
Validate the consistency and completeness of your modeled requirements before starting the design process.
Detect Run-Time and Diagnostic Errors
Prior to running simulations, you can identify run-time and modeling issues such as integer overflows, division by zero, out-of-bounds array access, subnormal values, floating-point inaccuracies, and data validity errors.
Find Dead Logic
Identify model components that remain inactive during simulation and code execution.
Analyze Missing Test Coverage
Extend existing test cases to improve model coverage, including generated code, C/C++ code invoked in Simulink, and logic in Stateflow charts, ensuring thorough verification and addressing untested paths.
Verify Formal Safety Requirements
Use MATLAB, Simulink, and Stateflow to define formal safety requirements and verify that your design meets them.
Create Requirements-Based Test Cases
Derive test cases based on system requirement models.
