Get Started with 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 IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

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

Demonstrates how to isolate potential causes of dead logic using the sldvexCommonCausesOfDeadLogic model. Dead logic detection finds unreachable objectives in the model that cause the model element to remain inactive.

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.