设计验证器窗格
设计验证器窗格概述
指定分析选项并配置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$
是一个代表模型名称的标记。
提示
您可以使用以下参数自定义 Simulink Design Verifier 输出的名称和位置:
在 结果窗格上:
数据文件名
框架模型文件名
Simulink Test options > Test File name
在 报告窗格上:
报告文件名
输出模型的文件路径
在 模块替换窗格上:
输出模型的文件路径
命令行信息
参数: DVOutputDir |
类型:字符数组 |
值:任何有效路径 |
默认: 'sldv_output/$ModelName$' |
另请参阅
通过添加后缀使输出文件名唯一
指定 Simulink Design Verifier 是否通过附加数字后缀使其输出文件名唯一。
设置
默认:在
- 开启
在 Simulink Design Verifier 输出文件名后附加增量数字后缀。选择此选项可防止软件覆盖具有相同名称的现有文件。
- 关闭
不为 Simulink Design Verifier 输出文件名附加后缀。在这种情况下,软件可能会覆盖具有相同名称的现有文件。
命令行信息
参数: DVMakeOutputFilesUnique |
类型:字符数组 |
值: 'on' | 'off' |
默认: 'on' |
另请参阅
检查模型兼容性
运行检查来评估您的模型是否与Simulink Design Verifier兼容。有关更多信息,请参阅 Simulink Design Verifier 检查 。
生成测试/检测错误/证明属性
当您设置模式参数时,此按钮会发生如下变化:
模式:测试生成,按钮内容为:生成测试
有关更多信息,请参阅 什么是测试用例生成? 。
模式:设计错误检测,按钮内容为:检测错误
有关更多信息,请参阅 什么是设计错误检测? 。
模式:属性证明,按钮内容为:证明属性
有关更多信息,请参阅 什么是财产证明? 。
重建模型表示
指定是否重建Simulink Design Verifier分析的模型表示。
设置
默认:如果检测到更改
- 始终
始终重建模型表示。
- 如果检测到更改
仅当软件检测到模型中有任何变化时才重建模型表示。
命令行信息
参数: DVRebuildModelRepresentation |
类型: character array |
值: 'Always' | 'IfChangeIsDetected' |
默认: 'If change is detected' |
另请参阅
自动桩件不受支持的模块和功能
指定在分析过程中是否忽略不受支持的模块和功能。
设置
默认:在
- 开启
忽略不受支持的模块和功能并继续分析。
- 关闭
当Simulink Design Verifier遇到不受支持的模块或函数时显示警告并询问您是否要继续分析。
命令行信息
参数: DVAutomaticStubbing |
类型:字符数组 |
值: 'on' | 'off' |
默认: 'on' |
另请参阅
在分析中支持 S 函数
指定是否启用对已编译为与 Simulink Design Verifier 兼容的 S-Function 的支持。
设置
默认:在
- 开启
启用对已编译为与 Simulink Design Verifier 兼容的 S-Function 的支持。
- 关闭
Simulink Design Verifier 在分析过程中自动桩件 S 函数。
命令行信息
参数: DVSFcnSupport |
类型:字符数组 |
值: 'on' | 'off' |
默认: 'on' |
另请参阅
使用指定的输入最小值和最大值
指定是否生成将指定的最小值和最大值视为模型中所有输入信号的约束的测试用例。
设置
默认:在
- 开启
将指定的最小值和最大值视为所有输入信号的约束。
- 关闭
忽略任何指定的最小值和最大值。
命令行信息
参数: DVDesignMinMaxConstraints |
类型:字符数组 |
值: 'on' | 'off' |
默认: 'on' |
另请参阅
运行附加分析以减少有理近似的情况
指定Simulink Design Verifier是否尝试在分析过程中减少有理近似的使用。
设置
默认:在
- 开启
当您使用 Simulink Design Verifier 分析模型时,如果模型符合以下情况,Simulink Design Verifier 会尝试减少有理近似的使用。启用此设置可能会增加分析时间。
- 关闭
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™ Manager 中的 functional testing and coverage analysis 等跨产品功能不支持并行计算进行验证。有关更多信息,请参阅 执行功能测试并分析测试覆盖率 (Simulink Test) 。
设置
默认:离开
- 开启
如果您拥有 Parallel Computing Toolbox 许可证,那么 Simulink Design Verifier 会在同一台机器上的多个工作程序上并行验证测试用例或反例。
- 关闭
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 函数的任何有效选项 |
默认值: '' |
根据过滤器忽略目标
指定分析模型,忽略过滤器文件中的目标。过滤器文件 包含您想要从分析中过滤的测试生成、死逻辑检测和设计错误检测目标的模型覆盖率目标。
设置
默认:离开
- 开启
在测试生成和设计错误检测分析期间忽略过滤器文件中的目标。
- 关闭
在测试生成和设计错误检测分析期间生成所有目标的结果,包括 过滤器文件 中的结果。
依赖
此参数启用 过滤器文件 。
命令行信息
参数: DVCovFilter |
类型:字符数组 |
值: 'on' | 'off' |
默认: 'off' |
另请参阅
覆盖率过滤 (Simulink Coverage)
过滤文件
为包含要从分析中过滤的模型覆盖率目标和设计错误检测目标的文件指定文件夹和文件名。
设置
默认值: ''
指定包含您想要从测试生成和设计错误检测分析中忽略的目标的文件夹名称和文件名。
单击过滤器资源管理器按钮加载现有的过滤器文件或创建新文件。
命令行信息
参数: DVCovFilterFileName |
类型:字符数组 |
值: 用逗号或分号分隔的有效文件路径 |
默认值: '' |
另请参阅
覆盖率过滤规则和文件 (Simulink Coverage)
筛选器资源管理器
单击“过滤器资源管理器”加载包含您想要在设计错误检测和测试生成分析中忽略的目标的文件。
依赖
此按钮由 基于过滤器忽略目标 启用。