# Specify and Verify Design Requirements

Verify design against requirements, refine counterexamples by using input
assumptions

Safety requirements define undesired behaviors in a model. Simulink^{®}
Design Verifier™ uses property proving to verify that properties associated
with model requirements hold under all
possible input values or provides counterexamples that lead to violations.
You use Simulink
Design Verifier to model design requirements as properties and then Prove Properties in a Model.

## Blocks

## Functions

## Topics

### Start Here

**Workflow for Proving Model Properties**

Outlines a process for proving properties of your model.**What Is Property Proving?**

Brief overview of proving properties.**Prove Properties in a Model**

Provides an example that walks you through the process of proving model properties.**Use Parameter Table to Find Constraints**

An example of how to specify parameters as variables for analysis.**Specify Signal Ranges**

Specify the minimum and maximum value that a signal can attain during simulation. Fully specify your design and optimize data types and the generated code by specifying the minimum and maximum value that a signal can attain during simulation.**Minimum and Maximum Input Constraints**

An overview of how the Simulink Design Verifier analysis considers specified input minimum and maximum values.**Specify Input Ranges on Simulink and Stateflow Elements**

Describes how the analysis handles minimum and maximum values on Simulink and Stateflow^{®}elements.**Verify and Validate a Model and Code**

Define requirements, test models and code, check for design errors and standards compliance, and measure test coverage.

### Requirements Modeling for Verification and Validation

**Construct Specification Models by Using Requirements Table Blocks**

Learn about specification models and how to use them for requirements-based verification.*(Since R2022b)***Model Requirements**

The Simulink Design Verifier block library includes a sublibrary Example Properties.**Isolate Verification Logic with Observers**

Describes the observer support for Simulink Design Verifier.**Specify Input Ranges on Simulink and Stateflow Elements**

Describes how the analysis handles minimum and maximum values on Simulink and Stateflow elements.**Use Specification Models for Requirements-Based Testing**

Follow a systematic approach to verify your design model against requirements.*(Since R2022b)*

### Verification by Property Proving

**Prove Properties in a Model**

Provides an example that walks you through the process of proving model properties.**Design and Verify Properties in a Model**

You can use Simulink® Design Verifier™ to model design requirements as properties and then prove properties in a model.**Debug Property Proving Violations by Using Model Slicer**

Use Model Slicer to debug your design with assertion blocks.**Prove System-Level Properties Using Verification Model**

An example that uses a verification model to prove system-level properties.**Prove Properties in a Subsystem**

Explains how to prove properties in a subsystem.**Check for Specified Minimum and Maximum Value Violations**

Describes how to analyze the model to verify that specified design minimum and maximum values are honored.**Specification of Input Ranges in sldvData Fields**

Describes the`sldvData`

fields for minimum and maximum input values.**Property Proving Using MATLAB Function Block**

This example shows how to verify the seat belt reminder design model.**Property Proving Using MATLAB Truth Table Block**

This example shows how to verify the seat belt reminder design model referenced in the top block above.**Property Proving with an Assumption Block**

This example shows how to perform a Simulink® Design Verifier™ property proof using a Proof Assumption block.**Property Proving with an Invalid Property**

This example shows how to find an invalid property using Simulink® Design Verifier™ property proving analysis.**Prove Properties in Large Models**

Describes workflows and best practices for proving properties in large models.