本页采用了机器翻译。点击此处可查看最新英文版本。

Simulink Design Verifier 检查

Simulink Design Verifier 检查概述

这些检查可帮助您为 Simulink® Design Verifier™ 分析准备模型。当您运行 Simulink Design Verifier 检查时，模型顾问会检查 Simulink Design Verifier 许可证。

有关模型顾问的更多信息，请参阅运行模型顾问检查 和 自动执行模型顾问检查。

Simulink Design Verifier 兼容性检查

Simulink Design Verifier 检查可帮助您通过识别模型中可能需要特别注意的元素来为 Simulink Design Verifier 分析做好模型准备。

当您运行 Simulink Design Verifier 检查时，模型顾问会执行 Simulink Design Verifier 许可证的检出。

使用模型顾问，您可以将检查结果保存在 HTML 文件中。请参阅Save and View Model Advisor Check Reports。有关使用模型顾问的更多信息，请参阅运行模型顾问检查。有关定制模型顾问的更多信息，请参阅自动执行模型顾问检查。

检查与 Simulink Design Verifier 的兼容性

检查 ID：mathworks.sldv.compatibility

识别 Simulink Design Verifier 分析不支持的元素。

描述

此项检查评估您的模型是否与 Simulink Design Verifier 兼容。

结果和建议的操作

情形建议采取的操作
不兼容

避免在您想要分析的模型或模型组件中使用以下不受支持的软件功能或 Simulink 模块：

部分兼容
兼容的Simulink Design Verifier 可以分析您的模型。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

Simulink Design Verifier 设计错误检查

Simulink Design Verifier 检查可帮助您通过识别模型中可能需要特别注意的元素来为 Simulink Design Verifier 分析做好模型准备。

当您运行 Simulink Design Verifier 检查时，模型顾问会执行 Simulink Design Verifier 许可证的检出。

使用模型顾问，您可以将检查结果保存在 HTML 文件中。请参阅Save and View Model Advisor Check Reports。有关使用模型顾问的更多信息，请参阅运行模型顾问检查。有关定制模型顾问的更多信息，请参阅自动执行模型顾问检查。

检测死逻辑

检查 ID：mathworks.sldv.deadlogic

识别在仿真中保持非活动的逻辑。

描述

此项检查可识别模型中在仿真中保持非活动的部分。

您可以运行更详细的分析，使用 Simulink Design Verifier 设计错误检测来识别死逻辑和活动逻辑。有关详细信息，请参阅 检测由错误值导致的死逻辑。

遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C 和 CWE 标准的代码的可能性

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅：

另请参阅 使用自动插桩处理不兼容问题。

模型中发现死逻辑Simulink Design Verifier 证明了这些决策和条件结果不可能发生并且是模型中的死逻辑。死逻辑也可能是对参数指定约束或对输入端口指定最小和最大约束的副作用。在极少数情况下，Simulink Design Verifier 执行的近似计算可能会导致死逻辑。可能存在本次分析未确定的目标。为了扩展此分析的结果，请使用 Simulink Design Verifier 设计错误检测来识别活动逻辑。从 Simulink 编辑器中选择 App > Design Verifier > 设置。在配置参数窗格的 Design Verifier > 设计错误检测 窗格中，选择死逻辑(部分) 或将 DVDetectDeadLogic 和 DVDetectActiveLogic 设置为 on。
模型中未发现死逻辑Simulink Design Verifier 未在模型中发现死逻辑。可能存在本次分析未确定的目标。为了扩展此分析的结果，请使用 Simulink Design Verifier 设计错误检测来识别活动逻辑。从 Simulink 编辑器中选择 App > Design Verifier > 设置。在配置参数窗格的 Design Verifier > 设计错误检测 窗格中，选择死逻辑(部分) 或将 DVDetectDeadLogic 和 DVDetectActiveLogic 设置为 on。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测超出范围的数组访问

检查 ID：mathworks.sldv.arraybounds

检测超出数组索引范围的访问操作

描述

此检查检测 Simulink Design Verifier 中超出边界的数组访问实例。

遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C、CWE、ISO/IEC TS 17961 标准的代码的可能性。

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅

另请参阅 使用自动插桩处理不兼容问题。

在模型中发现超出范围的数组访问

要查看导致越界数组访问的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。点击模型顾问报告中的查看测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测除以零

检查 ID：mathworks.sldv.divbyzero

检测模型中的除以零错误

描述

此检查可识别模型中除以零错误的操作。

遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C、CWE、ISO/IEC TS 17961 标准的代码的可能性。

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅

另请参阅 使用自动插桩处理不兼容问题。

在模型中发现除以零

要查看导致除以零的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。点击模型顾问报告中的查看测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测整数溢出

检查 ID：mathworks.sldv.integeroverflow

检测模型中的整数或定点数据溢出错误

描述

此检查可识别超出整数或定点运算的数据类型范围的运算。

遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C、CWE、ISO/IEC TS 17961 标准的代码的可能性。

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅

另请参阅 使用自动插桩处理不兼容问题。

模型中发现整数溢出

要查看导致整数溢出的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。点击模型顾问报告中的查看测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测非有限和 NaN 浮点值

检查 ID：mathworks.sldv.infnan

检测模型中的非有限和 NaN 浮点值

描述

此检查可检测模型中非有限和 NaN 浮点值的出现情况。

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅

另请参阅 使用自动插桩处理不兼容问题。

在模型中发现非有限和 NaN 浮点值

要查看导致出现非有限和 NaN 浮点值的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。点击模型顾问报告中的查看测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测低于正常的浮点值

检查 ID：mathworks.sldv.subnormal

检测模型中的次正常浮点值

描述

此检查可检测模型中是否出现低于正常的浮点值。

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅

另请参阅 使用自动插桩处理不兼容问题。

在模型中发现低于正常的浮点值

要查看导致出现低于正常值的浮点值的条件，请创建一个框架模型。当您仿真框架时，输入会复制错误。点击模型顾问报告中的查看测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测指定最小值和最大值违规

检查 ID：mathworks.sldv.minmax

检测超出指定最小值和最大值的信号

描述

该分析检查整个模型的中间信号和输出端口上指定的最小值和最大值（设计范围）。如果分析检测到信号超出了设计范围，结果将确定模型中出现错误的位置。

遵循此检查的建议可增加为嵌入式应用程序生成符合 MISRA C:2012 的代码以及符合 CERT C 和 CWE 标准的代码的可能性。

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅

另请参阅 使用自动插桩处理不兼容问题。

违反模型中的最小值和/或最大值

要查看导致违规的情况，请创建框架模型。当您仿真框架时，输入会复制错误。点击模型顾问报告中的查看测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测数据存储访问违规

检查 ID：mathworks.sldv.dsmaccessviolations

检测模型中的数据存储访问冲突。

描述

此项检查检测到以下数据存储访问冲突：

  • 写前读

  • 读后写

  • 写后写

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅：

发现数据存储访问违规

在模型顾问报告中，点击查看测试用例。该软件创建一个框架模型，并且 Signal Editor 模块显示复制错误的测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检测模块输入范围违规

检查 ID：mathworks.sldv.blockinputrangeviolations

检测模型中的模块输入范围违规。

描述

此检查检测具有以下设置的模块的输入范围违规：

注意

当插值方法设置为 Akima 样条或三次样条时，检查不会标记 n-D Lookup Table 模块的模块输入范围违规。

结果和建议的操作

结果建议采取的操作
失败，模型不兼容

解决模型不兼容问题。请参阅：

发现模块输入范围违规

在模型顾问报告中，点击查看测试用例。该软件创建一个框架模型，并且 Signal Editor 模块显示复制错误的测试用例。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检查 rem 和倒数运算的用法

检查 ID：mathworks.sldv.hismviolationshisl_0002

描述

识别导致非有限结果的 rem 和 reciprocal 运算的使用情况。

结果和建议的操作

情形建议采取的操作
模型或子系统包含可能导致非有限输出信号的 rem 或 reciprocal 操作。实时嵌入式系统不支持非有限信号。当使用 rem 或 reciprocal 操作时，保护相应的输入不等于零。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检查 Sqrt 运算的使用情况

检查 ID：mathworks.sldv.hismviolationshisl_0003

描述

识别输入可以为负数的 Sqrt 运算。

结果和建议的操作

情形建议采取的操作
模型中的一个或多个 Sqrt 操作的输入在仿真中可能会变为负值。重塑以保护 Sqrt 操作的输入不会变为负值。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检查 log 和 log10 运算的使用情形

检查 ID：mathworks.sldv.hismviolationshisl_0004

描述

识别导致非有限结果的 log 和 log10 操作。

结果和建议的操作

情形建议采取的操作
模型中使用的一个或多个 log 和 log10 操作可能需要非有限数支持，而实时嵌入式系统不支持这种支持。考虑保护这些操作的输入，使其不小于或等于零。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅

检查 Reciprocal Sqrt 模块的使用情形

检查 ID：mathworks.sldv.hismviolationshisl_0028

描述

识别输入可以为零或负数的 Reciprocal Sqrt 模块。

结果和建议的操作

情形建议采取的操作
模型中的一个或多个 Reciprocal Sqrt 模块的输入在仿真中可以变为零或负值。重新建模以保护 Reciprocal Sqrt 模块的输入不会变为负面。

功能和限制

  • 无法对库模型运行。

  • 分析封装子系统中的内容。默认情况下，将输入参数 Look under masks 设置为 all。

  • 分析库链接模块的内容。默认情况下，将输入参数 Follow links 设置为 on。

  • 不支持排除项。

另请参阅