Simulink Design Verifier Options

Simulink^® Design Verifier™ provides a comprehensive set of options to control and customize the verification and validation process of Simulink models. The options cover a broad spectrum of functionalities, including but not limited to, selecting the type of analysis by defining the search depth for errors, setting time and resource limits, and customizing test case generation for achieving different coverage metrics.

Options in Configuration Parameters Dialog Box

You can set options for Simulink Design Verifier analysis in the Configuration Parameters dialog box. To view the options, open Design Verifier tab. In the Prepare section, from the drop-down list and click Settings to open the Design Verifier pane of the model configuration parameters.

By default, options for Simulink Design Verifier do not appear in the Configuration Parameters dialog box. When you open the Design Verifier tab, Simulink Design Verifier associates its default options with the model. After you save the model, you can access options for Simulink Design Verifier directly from the Configuration Parameters dialog box.

See Set Model Configuration Parameters for a Model for more information about working with this interface.

Design Verification Options Objects

You can use the sldvoptions function to specify Simulink Design Verifier options at the command line.

To view the options associated with a Simulink model, type this syntax in the MATLAB^® command window:

opts = sldvoptions('model_name');
get(opts)

Command-Line Parameters for Design Verification Options

Use the following parameters to configure the behavior of Simulink Design Verifier. Use the get_param and set_param functions to retrieve and specify values for these parameters programmatically.

This table groups parameters based on a specific workflow and location in the Simulink Design Verifier options dialog box.

Pane	Options	UI Label	Commandline Parameter	Values
Design Verifier	Analysis options	Mode	DVMode	{'TestGeneration'} | 'DesignErrorDetection' | 'PropertyProving'
		Maximum analysis time (s)	DVMaxProcessTime	double {300}
	Output	Output folder	DVOutputDir	character array {'sldv_output/$ModelName$'}
		Make output file names unique by adding a suffix	DVMakeOutputFilesUnique	{'on'} | 'off'
	Rebuild model representation	Rebuild model representation	DVRebuildModelRepresentation	'Always' | {'If change is detected'}
		Automatic stubbing of unsupported blocks and functions	DVAutomaticStubbing	{'on'} | 'off'
		Use specified input minimum and maximum values	DVDesignMinMaxConstraints	{'on'} | 'off'
		Run additional analysis to reduce instances of rational approximation	DVReduceRationalApprox	{'on'} | 'off'
		Validate test cases or counterexamples with parallel computing	DVUseParallel	'on' | {'off'}
	Exclude and justify objectives	Ignore objectives based on filter	DVCovFilter	'on' | {'off'}
		Filter file(s)	DVCovFilterFileName	character array {''}
		Filter Explorer	DVCovFilterFileName
	Code analysis options	Support S-Functions in the analysis	DVSFcnSupport	{'on'} | off'
		Ignore the volatile qualifier	DVCodeAnalysisIgnoreVolatile	{'on'} | off'
		Additional options for code analysis	DVCodeAnalysisExtraOptions	character array {''}
Block Replacements	Block Replacements	Apply block replacements	DVBlockReplacement	'on' | {'off'}
		List of block replacement rules	DVBlockReplacementRulesList	character array {'<FactoryDefaultRules>'}
	Output model	File path of the output model	DVBlockReplacementModelFileName	character array {'$ModelName$_replacement'}
Parameters and Variants	Parameters	Parameter configuration	DVParameterConfiguration
		Parameter specification > Parameter table	DVParameterNames	double array {[]}
			DVParameterConstraints	double array {[]}
			DVParameterUseInAnalysis	cell array {[]}
		Parameter specification > Parameter table > Parameter configuration file	DVParametersConfigFileName	character array {'sldv_params_template.m'}
	Variants	Analyze all Startup Variants	DVAnalyzeAllStartupVariants
Test Generation	Test Generation	Test generation target	DVTestgenTarget	{'Model'} | 'GenCodeTopModel' | 'GenCodeModelRef'
		Model coverage objectives	DVModelCoverageObjectives	'None' | 'Decision' | {'ConditionDecision'} | 'MCDC' | 'EnhancedMCDC'
		Test conditions	DVTestConditions	'EnableAll' | 'DisableAll' | {'UseLocalSettings'}
		Test objectives	DVTestObjectives	'EnableAll' | 'DisableAll' | {'UseLocalSettings'}
		Maximum test case steps	DVMaxTestCaseSteps	int32 {10000}
		Test suite optimization	DVTestSuiteOptimization	{'Auto'} | 'IndividualObjectives' | 'LongTestcases' | 'LargeModel (Nonlinear Extended)'
	Relational Boundary Objectives	Include relational boundary	DVIncludeRelationalBoundary	{'on'} | 'off'
		Floating point absolute tolerance	DVAbsoluteTolerance	double {'1.0e-05'}
		Floating point relative tolerance	DVRelativeTolerance	double {'0.01'}
	Enhanced MCDC	Use strict propagation conditions	DVStrictEnhancedMCDC	'on' | {'off'}
	Add tests for the missing coverage	Extend using existing coverage data	DVIgnoreCovSatisfied	'on' | {'off'}
		Coverage data	DVCoverageDataFile	character array {''}
		Extend using existing test data	DVExtendExistingTests	'on' | {'off'}
		Test data	DVExistingTestFile	character array {''}
		Separate objectives satisfied with the existing tests/coverage data in the report	DVIgnoreExistTestSatisfied	{on'}| 'off'
Design Error Detection	Modeling Errors	Dead logic (partial)	DVDetectDeadLogic	'on' | {'off'}
		Run exhaustive analysis	DVDetectActiveLogic	'on' | {'off'}
		Coverage objectives to be analyzed	DVDeadLogicObjectives	'Decision' | {'ConditionDecision'} | 'MCDC'
		Out of bound array access	DVDetectOutOfBounds	{'on'} | 'off'
		Data store access violations	DVDetectDSMAccessViolations	'on' | {'off'}
	Numerical Errors	Division by zero	DVDetectDivisionByZero	{'on'} | 'off'
		Integer overflow	DVDetectIntegerOverflow	{'on'} | 'off'
		Non-finite and NaN floating-point values	DVDetectInfNaN	'on' | {'off'}
		Subnormal floating-point values	DVDetectSubnormal	'on' | {'off'}
	Signal Range Errors	Specified minimum and maximum value violations	DVDesignMinMaxCheck	'on' | {'off'}
		Specified block input range violations	DVDetectBlockInputRangeViolations	'on' | {'off'}
	High-Integrity Systems Modeling Checks	Usage of remainder and reciprocal operations - hisl_0002	DVDetectHISMViolationsHisl_0002
		Usage of square root operations - hisl_0003	DVDetectHISMViolationsHisl_0003
		Usage of log and log10 operations - hisl_0004	DVDetectHISMViolationsHisl_0004
		Usage of Reciprocal Square Root blocks - hisl_0028	DVDetectHISMViolationsHisl_0028
Property Proving	Property Proving	Assertion blocks	DVAssertions	'EnableAll' | 'DisableAll' | {'UseLocalSettings'}
		Proof assumptions	DVProofAssumptions	'EnableAll' | 'DisableAll' | {'UseLocalSettings'}
		Strategy	DVProvingStrategy	'FindViolation' | {'Prove'} | 'ProveWithViolationDetection'
		Maximum violation steps	DVMaxViolationSteps	int32 {'20'}
Results	Data file options	Data file name	DVDataFileName	character array {'$ModelName$_sldvdata'}
		Include expected output values	DVSaveExpectedOutput	'on' | {'off'}
		Randomize data that do not affect the outcome	DVRandomizeNoEffectData	'on' | {'off'}
	Harness model options	Generate separate harness model after analysis	DVSaveHarnessModel	'on' | {'off'}
		Harness model file name	DVHarnessModelFileName	character array {'$ModelName$_harness'}
		Reference input model in generated harness	DVModelReferenceHarness	'on' | {'off'}
		Harness source	DVHarnessSource	{'Signal Builder'} | 'Signal Editor'
	Simulink Test options	Test File name	DVSlTestFileName	character array {'$ModelName$_test'}
		Test Harness name	DVSlTestHarnessName	character array {'$ModelName$_sldvharness'}
Report	Report	Generate report of the results	DVSaveReport	'on' | {off'}
		Generate additional report in PDF format	DVReportPDFFormat	'on' | {off'}
		Report file name	DVReportFileName	character array {'$ModelName$_report'}
		Include screen shots of properties	DVReportIncludeGraphics	'on' | {off'}
		Display report	DVDisplayReport	{'on'} | 'off'

Related Topics

• Design Verifier Pane
• sldvoptions