设置 Simulink Design Verifier 分析选项
Simulink® Design Verifier™ 提供了一组全面的选项来控制和自定义 Simulink 模型的验证和确认过程。这些选项涵盖了广泛的功能，包括但不限于通过定义错误的搜索深度来选择分析类型、设置时间和资源限制以及自定义测试用例生成以实现不同的覆盖率度量。
“配置参数”对话框中的选项
您可以在“配置参数”对话框中设置 Simulink Design Verifier 分析的选项。要查看选项，请打开 Design Verifier 选项卡。在准备部分中，从下拉列表中点击设置以打开模型配置参数的 Design Verifier 窗格。
默认情况下，Simulink Design Verifier 的选项不会显示在“配置参数”对话框中。当您打开 Design Verifier 选项卡时，Simulink Design Verifier 会将其默认选项与模型关联。您保存模型后，可以直接从“配置参数”对话框访问 Simulink Design Verifier 的选项。
有关使用此界面的详细信息，请参阅为模型设置模型配置参数。
设计验证选项对象
您可以使用 sldvoptions 函数在命令行中指定 Simulink Design Verifier 选项。
要查看与 Simulink 模型关联的选项，请在 MATLAB® 命令行窗口中键入以下语法：
opts = sldvoptions('model_name');
get(opts)设计验证选项的命令行参数
使用以下参数配置 Simulink Design Verifier 的行为。使用 get_param 和 set_param 函数以编程方式检索和指定这些参数的值。
下表基于 Simulink Design Verifier 选项对话框中的特定工作流和位置对参数进行了分组。
| 窗格 | 选项 | UI 标签 | 命令行参数 | 值 |
|---|---|---|---|---|
| Design Verifier | 分析选项 | 模式 |
|
|
最长分析时间(s) |
| 双精度 | ||
| 输出 | 输出文件夹 |
| 字符数组 | |
| 通过添加后缀使输出文件名具有唯一性 | DVMakeOutputFilesUnique | {'on'} | 'off' | ||
| 重新编译模型表示 | 重新编译模型表示 | DVRebuildModelRepresentation | 'Always' | {'If change is detected'} | |
| 不支持的模块和函数的自动插桩 | DVAutomaticStubbing | {'on'} | 'off' | ||
| 使用指定的输入最小值和最大值 | DVDesignMinMaxConstraints | {'on'} | 'off' | ||
| 运行附加分析以减少有理逼近的实例 | DVReduceRationalApprox | {'on'} | 'off' | ||
| 通过并行计算验证测试用例或反例 | DVUseParallel | 'on' | {'off'} | ||
| 排除和申述目标 | 根据过滤器忽略目标 | DVCovFilter | 'on' | {'off'} | |
| 过滤器文件 | DVCovFilterFileName | 字符数组 | ||
| 过滤器资源管理器 | DVCovFilterFileName | |||
| 代码分析选项 | 在分析中支持 S-Function | DVSFcnSupport | {'on'} | off' | |
| 忽略 volatile 限定符 | DVCodeAnalysisIgnoreVolatile | {'on'} | off' | ||
| 代码分析附加选项 | DVCodeAnalysisExtraOptions | character array {''} | ||
| 模块替换 | 模块替换 | 应用模块替换 | DVBlockReplacement |
|
| 模块替换规则列表 | DVBlockReplacementRulesList | 字符数组 {'<FactoryDefaultRules>'} | ||
| 输出模型 | 输出模型的文件路径 | DVBlockReplacementModelFileName | 字符数组 {'$ModelName$_replacement'} | |
| 参数和变体 | 参数 | 参数配置 | DVParameterConfiguration | |
| 参数设定 > 参数表 | DVParameterNames | 双精度数组 {[]} | ||
DVParameterConstraints | 双精度数组 {[]} | |||
DVParameterUseInAnalysis | 元胞数组 {[]} | |||
| 参数设定 > 参数表 > 参数配置文件 | DVParametersConfigFileName | 字符数组 {'sldv_params_template.m'} | ||
| 变体 | 分析所有启动变体 | DVAnalyzeAllStartupVariants | ||
| 测试生成 | 测试生成 | 测试生成目标 | DVTestgenTarget | {'Model'} | 'GenCodeTopModel' | 'GenCodeModelRef' |
| 模型覆盖率目标 | DVModelCoverageObjectives | 'None' | 'Decision' | {'ConditionDecision'} | 'MCDC' | 'EnhancedMCDC' | ||
| 测试条件 | DVTestConditions | 'EnableAll' | 'DisableAll' | {'UseLocalSettings'} | ||
| 测试目标 | DVTestObjectives | 'EnableAll' | 'DisableAll' | {'UseLocalSettings'} | ||
| 最大测试用例步数 | DVMaxTestCaseSteps | int32 {10000} | ||
| 测试套件优化 | DVTestSuiteOptimization | {'Auto'} | 'IndividualObjectives' | 'LongTestcases' | 'LargeModel (Nonlinear Extended)' | ||
| 关系边界目标 | 包括关系边界目标 | DVIncludeRelationalBoundary | {'on'} | 'off' | |
| 浮点绝对容差 | DVAbsoluteTolerance | 双精度 {'1.0e-05'} | ||
| 浮点相对容差 | DVRelativeTolerance | 双精度 {'0.01'} | ||
| 增强的 MCDC | 使用严格传播条件 | DVStrictEnhancedMCDC | 'on' | {'off'} | |
| 针对缺失覆盖率添加测试 | 使用现有覆盖率数据进行扩展 | DVIgnoreCovSatisfied | 'on' | {'off'} | |
| 覆盖率数据 | DVCoverageDataFile | 字符数组 {''} | ||
| 使用现有测试数据进行扩展 | DVExtendExistingTests | 'on' | {'off'} | ||
| 测试数据 | DVExistingTestFile | 字符数组 {''} | ||
| 报告中的现有测试/覆盖率数据满足的单独目标 | DVIgnoreExistTestSatisfied | {on'}| 'off' | ||
| 设计错误检测 | 缺陷检查器 | DVDefectChecker | {'on'} | 'off' | |
| 建模错误 | 死逻辑(部分) | DVDetectDeadLogic | 'on' | {'off'} | |
| 运行穷举分析 | DVDetectActiveLogic | 'on' | {'off'} | ||
| 要分析的覆盖率目标 | DVDeadLogicObjectives | 'Decision' | {'ConditionDecision'} | 'MCDC' | ||
| 越界数组访问 | DVDetectOutOfBounds | {'on'} | 'off' | ||
| 数据存储访问违规 | DVDetectDSMAccessViolations | 'on' | {'off'} | ||
| 数值错误 | 除以零 | DVDetectDivisionByZero | {'on'} | 'off' | |
| 整数溢出 | DVDetectIntegerOverflow | {'on'} | 'off' | ||
| 非有限值和 NaN 浮点值 | DVDetectInfNaN | 'on' | {'off'} | ||
| 次正规浮点值 | DVDetectSubnormal | 'on' | {'off'} | ||
| 信号范围错误 | 指定的最小值和最大值违规 | DVDesignMinMaxCheck | 'on' | {'off'} | |
| 指定的模块输入范围违规 | DVDetectBlockInputRangeViolations | 'on' | {'off'} | ||
| 高完整性系统建模检查 | 余数和倒数运算的使用 - hisl_0002 | DVDetectHISMViolationsHisl_0002 | ||
| 平方根运算的使用 - hisl_0003 | DVDetectHISMViolationsHisl_0003 | |||
| log 和 log10 运算的使用 - hisl_0004 | DVDetectHISMViolationsHisl_0004 | |||
| Reciprocal Square Root 模块的使用 - hisl_0028 | DVDetectHISMViolationsHisl_0028 | |||
| 属性证明 | 属性证明 | Assertion 模块 | DVAssertions | 'EnableAll' | 'DisableAll' | {'UseLocalSettings'} |
| 证明假设 | DVProofAssumptions | 'EnableAll' | 'DisableAll' | {'UseLocalSettings'} | ||
| 策略 | DVProvingStrategy | 'FindViolation' | {'Prove'} | 'ProveWithViolationDetection' | ||
| 最大违规步数 | DVMaxViolationSteps | int32 {'20'} | ||
| 结果 | 数据文件选项 | 数据文件名 | DVDataFileName | 字符数组 {'$ModelName$_sldvdata'} |
| 包括预期的输出值 | DVSaveExpectedOutput | 'on' | {'off'} | ||
| 随机化不影响结果的数据 | DVRandomizeNoEffectData | 'on' | {'off'} | ||
| 框架模型选项 | 分析后生成单独的框架模型 | DVSaveHarnessModel | 'on' | {'off'} | |
| 框架模型文件名 | DVHarnessModelFileName | 字符数组 {'$ModelName$_harness'} | ||
| 生成的框架中的引用输入模型 | DVModelReferenceHarness | 'on' | {'off'} | ||
| Simulink Test 选项 | 测试文件名 | DVSlTestFileName | 字符数组 {'$ModelName$_test'} | |
| 测试框架名称 | DVSlTestHarnessName | 字符数组 {'$ModelName$_sldvharness'} | ||
| 报告 | 报告 | 生成结果报告 | DVSaveReport | 'on' | {off'} |
| 生成 PDF 格式的附加报告 | DVReportPDFFormat | 'on' | {off'} | ||
| 报告文件名 | DVReportFileName | 字符数组 {'$ModelName$_report'} | ||
| 包括属性的屏幕截图 | DVReportIncludeGraphics | 'on' | {off'} | ||
| 显示报告 | DVDisplayReport | {'on'} | 'off' |
