使用自动插桩处理不兼容问题

Simulink^® Design Verifier™ 中的插桩是指将模型的某些部分替换为更简单的表示或“桩件”以便于分析的过程。

通过自动插桩，您可以分析包含 Simulink Design Verifier 不支持的对象的模型。该方法使软件能够完成分析。

当 Simulink Design Verifier 分析遇到不受支持的模块时，软件会对该模块进行“插桩”。分析会忽略该模块的行为，因此，模块输出可以取任意值。

当函数参数设置为 acos 时，Simulink Design Verifier 不支持 Trigonometric Function 模块，如下图所示。

Trigonometric Function block for acos. The input goes through acos and output signal is viewed on the Scope

在分析过程中对该模块进行插桩时，out_signal 可以取任意值，结果如下。

分析模型	对 out_signal 进行插桩的结果
设计错误检测	如果依赖于 `out_signal` 的设计错误目标被证明有效，则该目标对所有仿真都有效。在这种情况下，插桩不会影响分析结果。如果依赖于 `out_signal` 的设计错误目标被证伪，则分析无法创建测试用例。分析无法确定被插桩的模块的哪个输入会生成导致目标被证伪的输出。
测试用例生成	如果依赖于 `out_signal` 的值的测试目标被满足，则分析无法创建测试用例。分析无法确定被插桩的模块的哪个输入会生成满足目标的输出。如果依赖于 `out_signal` 的值的测试目标无法满足，则不存在能够满足该目标的仿真。在这种情况下，插桩不会影响分析结果。
属性证明	如果依赖于 `out_signal` 的证明目标被证明有效，则该目标对所有仿真都有效。在这种情况下，插桩不会影响分析结果。如果依赖于 `out_signal` 的证明目标被证伪，则分析无法创建反例。分析无法确定被插桩的模块的哪个输入会生成导致目标被证伪的输出。

以下模型包含一个 Discrete State-Space 模块，该模块与 Simulink Design Verifier 不兼容。

Model containing a Discrete State-Space block and a saturation block.

如果您运行分析，请确保查看结果。在 Simulink Design Verifier 分析报告中，您可以看到 Simulink Design Verifier 遇到的不受支持的模块表。

不受支持的模块

为示例模型生成的分析报告显示，由于插桩，目标未决。Simulink Design Verifier 分析无法生成测试用例，因为它不理解 Discrete State-Space 模块的运算。

由于插桩而未决的目标

您可以定义自定义模块替换，以便更精确地定义不受支持的模块。有关详细信息，请按照不受支持的模块的模块替换中的步骤操作。