Get Started with Simulink Design Verifier

R2026b

Identify design errors, prove requirements compliance, and generate tests

Simulink^® Design Verifier™ uses formal methods to identify hidden design errors in models. It detects operations in models that result in runtime 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).

Acknowledgments

Tutorials

Use Simulink Design Verifier for Systematic Model Verification

Learn the basics of Simulink Design Verifier analysis.

Generate Test Cases for a Model

Prepare model, configure model settings, and review test generation analysis results.

STEP 1: Prepare Model for Test Generation Analysis
STEP 2: Configure Model Settings and Run Analysis
STEP 3: Review Test Generation Analysis Results

Detect Design Errors in a Model

Configure model settings, detect design errors, and review results.

STEP 1: Prepare Model for Design Error Detection Analysis
STEP 2: Detect Common Design Errors
STEP 3: Perform Design Error Detection Analysis
STEP 4: Review Design Error Detection Analysis Results
STEP 5: Fix Design Errors in Model

Featured Examples

Analyze Results for Dead Logic Analysis

Determine potential causes for dead logic in the analysis.

Open Script

Find and Debug Property Violation Using Simulink Design Verifier

Use Simulink Design Verifier to find and debug property violation in model.

Open Script

Use Specification Models for Requirements-Based Testing

Follow a systematic approach to verify your design model against requirements.

Since R2022b
Open Live Script

Videos

What Is Simulink Design Verifier?
Introduction to Simulink Design Verifier.

How to Use Simulink Design Verifier to Automatically Detect Design Errors in Your Simulink Models
Use Simulink Design Verifier to find errors in a design, and how errors, when detected, can be debugged using the visualization features in Simulink Design Verifier.

DO-178C Workflow for Automatic Test Vector Generation
Use Simulink Design Verifier to automatically generate test vectors to analyze missing model coverage collected by Simulink Coverage in order to comply with DO-178C and its supplements.

How to Debug a Property Proving Counterexample
Property proving with Simulink Design Verifier™ is a static analysis technique that uses formal methods to prove whether a given property will always be valid. This technique can help you formally verify that specific requirements implemented in your design will always be met.

Requirements-Based Testing Workflow
Explains how to create a test using a test sequence, define a formal assessment, link test cases to requirements, run test suites, and analyze missing model test coverage.