Design Verifier 窗格
Design Verifier 窗格概述
指定分析选项并配置 Simulink® Design Verifier™ 输出。
模式
指定 Simulink Design Verifier 的分析模式。
设置
默认值：测试生成
- 设计错误检测
检测模型中的整数和定点溢出错误以及除以零错误
- 测试生成
为模型生成测试用例。
- 属性证明
证明模型的属性。
提示
Simulink Design Verifier 指定当您从模式部分中的 Design Verifier 选项卡中选择以下分析选项之一时此选项的值：
选择设计错误检测，然后点击检测设计错误。
选择测试生成，然后点击生成测试。
选择属性证明，然后点击证明属性。
依赖关系
当设置模式参数时，检查模型兼容性下方的按钮发生如下变化：
模式：测试生成，按钮内容为：生成测试
模式：设计错误检测，按钮内容为：检测错误
模式：属性证明，按钮内容为：证明属性
命令行信息
参数：DVMode |
| 类型：字符数组 |
值：'TestGeneration' | 'DesignErrorDetection' | 'PropertyProving' |
默认值： 'TestGeneration' |
另请参阅
最大分析时间
指定 Simulink Design Verifier 分析模型所花费的最长时间（以秒为单位）。您可以将最大分析时间的值设置为您愿意提供给分析的值。您也可以随时停止分析。
设置
默认值： 300
您输入的值代表 Simulink Design Verifier 分析模型的最大秒数。
命令行信息
参数：DVMaxProcessTime |
类型：double |
| 值：任何有效值 |
默认值： 300 |
输出文件夹
指定 Simulink Design Verifier 写入其输出的路径名。
设置
默认值： sldv_output/$ModelName$
输入相对于当前文件夹的绝对路径或相对路径。
$ModelName$是一个代表模型名称的标记。$CacheFolder$是一个代表 Simulink 缓存文件夹的标记。
提示
您可以使用以下参数自定义 Simulink Design Verifier 输出的名称和位置：
在结果窗格上：
数据文件名
框架模型文件名
Simulink 测试选项 > 测试文件名
在报告窗格上：
报告文件名
输出模型的文件路径
在模块替换窗格上：
输出模型的文件路径
命令行信息
参数：DVOutputDir |
| 类型：字符数组 |
| 值：任何有效路径 |
默认值： 'sldv_output/$ModelName$' |
另请参阅
通过添加后缀使输出文件名具有唯一性
指定 Simulink Design Verifier 是否通过附加数字后缀使其输出文件名唯一。
设置
默认值：On
On在 Simulink Design Verifier 输出文件名后附加增量数字后缀。选择此选项可防止软件覆盖具有相同名称的现有文件。
Off不为 Simulink Design Verifier 输出文件名附加后缀。在这种情况下，软件可能会覆盖具有相同名称的现有文件。
命令行信息
参数：DVMakeOutputFilesUnique |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'on' |
另请参阅
检查模型兼容性
运行检查来评估您的模型是否与 Simulink Design Verifier 兼容。有关详细信息，请参阅Simulink Design Verifier 检查。
生成测试/检测错误/证明属性
当您设置模式参数时，此按钮会发生如下变化：
模式：测试生成，按钮内容为：生成测试
有关详细信息，请参阅测试生成工作流。
模式：设计错误检测，按钮内容为：检测错误
有关详细信息，请参阅 什么是设计错误检测？。
模式：属性证明，按钮内容为：证明属性
有关详细信息，请参阅 使用 Simulink Design Verifier 证明模型属性。
重新编译模型表示
指定是否重建 Simulink Design Verifier 分析的模型表示。
设置
默认值：如果检测到更改
- 始终
始终重建模型表示。
- 如果检测到更改
仅当软件检测到模型中有任何变化时才重建模型表示。
命令行信息
参数：DVRebuildModelRepresentation |
类型：character array |
值：'Always' | 'IfChangeIsDetected' |
默认值： 'If change is detected' |
另请参阅
不支持的模块和函数的自动插桩
指定在分析过程中是否忽略不受支持的模块和函数。
设置
默认值：On
- On
忽略不受支持的模块和函数并继续分析。
- Off
当 Simulink Design Verifier 遇到不受支持的模块或函数时显示警告并询问您是否要继续分析。
命令行信息
参数：DVAutomaticStubbing |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'on' |
另请参阅
在分析中支持 S-Function
指定是否启用对已编译为与 Simulink Design Verifier 兼容的 S-Function 的支持。
设置
默认值：On
- On
启用对已编译为与 Simulink Design Verifier 兼容的 S-Function 的支持。
- Off
Simulink Design Verifier 在分析过程中对 S-Function 进行自动插桩。
命令行信息
参数：DVSFcnSupport |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'on' |
另请参阅
忽略 volatile 限定符
指定易失性变量是否被视为普通变量或插桩变量。
设置
默认值：On
- On
C 代码中的易失性变量和参数与非易失性变量相同。
- Off
指示 C 代码中的易失性变量和参数是否必须引入占位符。
命令行信息
参数：DVCodeAnalysisIgnoreVolatile |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'on' |
另请参阅
使用指定的输入最小值和最大值
指定是否生成将指定的最小值和最大值视为模型中所有输入信号的约束的测试用例。
设置
默认值：On
- On
将指定的最小值和最大值视为所有输入信号的约束。
- Off
忽略任何指定的最小值和最大值。
命令行信息
参数：DVDesignMinMaxConstraints |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'on' |
另请参阅
运行附加分析以减少有理逼近的实例
指定 Simulink Design Verifier 是否尝试在分析过程中减少有理近似的使用。
设置
默认值：On
- On
当您使用 Simulink Design Verifier 分析模型时，如果模型符合以下情况，Simulink Design Verifier 会尝试减少有理近似的使用。启用此设置可能会增加分析时间。
- Off
Simulink Design Verifier 并不试图在分析过程中减少有理近似的使用。
命令行信息
参数：DVReduceRationalApprox |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'on' |
通过并行计算验证测试用例或反例
指定是否使用并行计算来验证测试用例或反例。此选项需要 Parallel Computing Toolbox™ 许可证。
何时使用并行计算进行验证
一般而言，如果满足以下条件，并行执行可以帮助减少验证时间：
您有一个复杂的 Simulink 模型，需要很长时间才能仿真。
Simulink Design Verifier 分析超出了最大分析时间，并导致多个目标处于“需要仿真”状态。有关详细信息，请参阅 目标满足 - 需求仿真 和 目标被证伪 - 需要仿真。
测试生成分析生成长测试用例。这可能是因为您将测试套件优化设置为 LongTestcases 或者最大测试用例步数值大于默认值。有关详细信息，请参阅 测试生成窗格概述。
使用并行计算进行验证时必须考虑以下几点：
启动并行池可能需要一些时间，这会影响整体分析时间。为了减少分析时间：
在运行测试生成分析之前，请确保并行池已经在运行。默认情况下，并行池在空闲指定的分钟数后会关闭。要更改设置，请参阅 Parallel Computing Toolbox 中的主题“指定您的并行预设项”。
在所有并行池工作进程上加载 Simulink。
仿真按以下顺序进行：
该集群不是
local。配置并行预设项以仅使用local集群。要更改设置，请参阅 Parallel Computing Toolbox 中的主题“指定您的并行预设项”。在启动 SLDV 分析之前，模型处于
dirty state状态。该模型有
ToFile模块。该模型是内部框架。
Simulink Test™ 管理器中的功能测试和覆盖率分析等跨产品功能不支持并行计算进行验证。有关详细信息，请参阅 执行功能测试并分析测试覆盖率 (Simulink Test)。
设置
默认值：Off
- On
如果您拥有 Parallel Computing Toolbox 许可证，那么 Simulink Design Verifier 会在同一台机器上的多个工作程序上并行验证测试用例或反例。
- Off
Simulink Design Verifier 连续验证测试用例或反例。
命令行信息
参数：DVUseParallel |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'off' |
另请参阅
代码分析附加选项
指定用于分析已编译为与 Simulink Design Verifier 兼容的 S-Function 的附加选项。有关详细信息，请参阅 S-Function 和 C/C++ 代码的支持限制和注意事项。
设置
默认值： ''
输入用于分析已编译为与 Simulink Design Verifier 兼容的 S-Function 的附加选项。例如，要指定数组的最大大小，请输入 defaultArraySize = 512。
命令行信息
参数：DVCodeAnalysisExtraOptions |
| 类型：字符数组 |
| 值： 用于分析 S-Function 的任何有效选项 |
默认值： '' |
根据过滤器忽略目标
指定分析模型，忽略过滤器文件中的目标。过滤器文件包含您想要从分析中过滤的测试生成、死逻辑检测和设计错误检测目标的模型覆盖率目标。
设置
默认值：Off
- On
在测试生成和设计错误检测分析期间忽略过滤器文件中的目标。
- Off
在测试生成和设计错误检测分析期间生成所有目标的结果，包括过滤器文件中的结果。
依赖关系
此参数启用过滤器文件。
命令行信息
参数：DVCovFilter |
| 类型：字符数组 |
值：'on' | 'off' |
默认值： 'off' |
另请参阅
覆盖率过滤 (Simulink Coverage)
过滤器文件
为包含要从分析中过滤的模型覆盖率目标和设计错误检测目标的文件指定文件夹和文件名。
设置
默认值： ''
指定包含您想要从测试生成和设计错误检测分析中忽略的目标的文件夹名称和文件名。
点击过滤器资源管理器按钮加载现有的过滤器文件或创建新文件。
命令行信息
参数：DVCovFilterFileName |
| 类型：字符数组 |
| 值： 用逗号或分号分隔的有效文件路径 |
默认值： '' |
另请参阅
覆盖率过滤规则和文件 (Simulink Coverage)
过滤器资源管理器
点击过滤器资源管理器加载包含您想要在设计错误检测和测试生成分析中忽略的目标的文件。
依赖关系
此按钮由基于过滤器忽略目标启用。
