Simulink Design Verifier - Documentation

Contents

Index

• Getting Started

• How the Simulink Design Verifier Software Works

Model Analysis with Simulink Design Verifier Software

Analyzing a Simple Model

Analyzing Large Models

• Handling Incompatibilities with Automatic Stubbing

What Is Automatic Stubbing?

Analyzing a Model Using Automatic Stubbing

• Approximations

Approximations During Model Analysis

Types of Approximations

Converting Floating-Point Arithmetic to Rational-Number Arithmetic

Linearizing 2-D Lookup Tables

Unrolling While Loops

Ensuring the Validity of the Analysis

• Ensuring Compatibility with the Simulink Design Verifier Software

• Checking Model Compatibility

Model Is Compatible

Model Is Incompatible

Some Model Elements Are Incompatible

• Unsupported Simulink Software Features

Simulink Software Features Not Supported

Simulink Block Support Limitations

Limitations of Support for Model Reference

Unsupported Stateflow Software Features

• Support Limitations for the Embedded MATLAB Subset

Unsupported Embedded MATLAB Subset Features

Limitations of Embedded MATLAB Library Function Support

Fixed-Point Support Limitations

• Working with Block Replacements

About Block Replacements

Built-In Block Replacements

Template for Block Replacement Rules

• Defining Custom Block Replacements

Basic Workflow for Defining Custom Block Replacements

Specifying Replacement Blocks

Writing Block Replacement Rules

Example: Replacing Multiport Switch Blocks

• Executing Block Replacements

Configuring Block Replacements

Replacing Blocks in a Model

• Specifying Parameter Configurations

About Parameter Configurations

Template for Parameter Configurations

Defining Parameter Configurations

• Parameter Configuration Example

About This Example

Constructing the Example Model

Parameterizing the Constant Block

Specifying a Parameter Configuration

Analyzing the Example Model

Simulating the Test Cases

• Configuring Simulink Design Verifier Options

Viewing Simulink Design Verifier Options

• Configuring Simulink Design Verifier Options

Design Verifier Pane

Block Replacements Pane

Parameters Pane

Test Generation Pane

Property Proving Pane

Saving Simulink Design Verifier Options

• Generating Test Cases

• About Test Case Generation

Test Case Blocks

Test Case Functions

Workflow for Generating Test Cases

• Generating Test Cases for a Model

About This Example

Constructing the Example Model

Checking Compatibility of the Example Model

Configuring Test Generation Options

Analyzing the Example Model

Customizing Test Generation

Reanalyzing the Example Model

Analyzing Contradictory Models

Generating Test Cases for a Subsystem

• Proving Properties of a Model

• About Property Proving

Proof Functions

Workflow for Proving Model Properties

• Proving Properties in a Model

About This Example

Constructing the Example Model

Checking Compatibility of the Example Model

Instrumenting the Example Model

Configuring Property-Proving Options

Analyzing the Example Model

Customizing the Example Proof

Reanalyzing the Example Model

Analyzing Contradictory Models

Proving Properties in a Subsystem

• Proving Complex Properties

Property-Proving Examples

• Reviewing the Results

• Examining Simulink Design Verifier Data Files

About Simulink Design Verifier Data Files

Overview of the sldvData Structure

Model Information Fields in sldvData

Simulating Models with Simulink Design Verifier Data Files

• Exploring Test Harness Models

About Test Harness Models

Anatomy of a Test Harness

Configuration of the Test Harness

Simulating the Test Harness

Creating a SystemTest TEST-File

• Understanding Simulink Design Verifier Reports

About Simulink Design Verifier Reports

Summary Chapter

Analysis Information Chapter

Test / Proof Objectives Status Chapter

Model Items Chapter

Test Cases / Properties Chapter

• Analyzing Large Models and Improving Performance

Sources of Model Complexity

• Analyzing a Large Model

Types of Large Model Problems

Using the Default Parameter Values

Modifying the Analysis Parameters

Using the Large Model Optimization

Stopping the Analysis Before Completion

Generating Reports for Large Models

• Managing Model Data to Simplify the Analysis

Simplifying Data Types

Constraining Data

Partitioning Model Inputs and Generating Tests Incrementally

Analyzing the Model Using a Bottom-Up Approach

Analyzing Logical Operations

Handling Models with Large State Spaces

Handling Problems with Counters and Timers

Techniques for Proving Properties of Large Models

• Configuration Parameters

• Design Verifier Pane

Design Verifier Pane Overview

Maximum analysis time

Display unsatisfiable test objectives

Automatic stubbing of unsupported blocks and functions

Output directory

Make output file names unique by adding a suffix

• Design Verifier Pane: Block Replacements

Block Replacements Pane Overview

Apply block replacements

List of block replacement rules

File path of the output model

• Design Verifier Pane: Parameters

Parameters Pane Overview

Apply parameters

Parameter configuration file

• Design Verifier Pane: Test Generation

Test Generation Pane Overview

Model coverage objectives

Test conditions

Test objectives

Maximum test case steps

Test suite optimization

• Design Verifier Pane: Property Proving

Property Proving Pane Overview

Assertion blocks

Proof assumptions

Maximum violation steps

• Design Verifier Pane: Results

Results Pane Overview

Save test data to file

Include expected output values

Randomize data that does not affect outcome

Save test harness as model

Harness model file name

Reference input model in generated harness

Save test harness as SystemTest TEST-file (will reference saved data file)

SystemTest file name

• Design Verifier Pane: Report

Report Pane Overview

Generate report of the results

Report file name

Include screen shots of properties and text objectives

Parameter Command-Line Information Summary

• Simulink Block Support

Overview of Simulink Block Support

Additional Math and Discrete Library

Commonly Used Blocks Library

Continuous Library

Discontinuities Library

Discrete Library

Logic and Bit Operations Library

Lookup Tables Library

Math Operations Library

Model Verification Library

Model-Wide Utilities Library

Ports & Subsystems Library

Signal Attributes Library

Signal Routing Library

Sources Library

User-Defined Functions Library

Embedded MATLAB Subset Support

• Release Notes

Simulink Design
Verifier roadmap page

	Functions:
	Alphabetical List

	Blocks:
	Alphabetical List



	Documentation Set

	Getting Started
	Introduces Simulink Design Verifier and gets you started using it

	User's Guide
	Provides tutorials and comprehensive information about Simulink Design Verifier

	Examples in Documentation
	Lists major examples in the Simulink Design Verifier documentation



	Product Demos

	Simulink Design Verifier Demos
	Presents a collection of demos that you can run from the Help browser to help you learn the product



	What's New

	Release Notes
	Summarizes new features, bug fixes, upgrade issues, etc.



	Printable (PDF) Documentation on the Web

PDF documents reflect the most recent version of Simulink Design Verifier and might describe features not available in earlier versions of the software.
	Simulink Design Verifier User's Guide
	Simulink Design Verifier Release Notes

The MathWorks Web Site Resources

	Demos
	MATLAB Central
	Product Page
	Platforms & Requirements

	Related Books
	Related Products
	Technical Support

© 1984-2009- The MathWorks, Inc. - Site Help - Patents - Trademarks - Privacy Policy - Preventing Piracy - RSS