Main Content

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

使用假设模块证明属性

打开脚本

此示例显示如何使用 Proof Assumption模块执行 Simulink® Design Verifier™属性证明。它试图证明，当当前输入值和之前的六个输入值的总和大于 6 时，输出等于 2。该模型包括一个Proof Assumption模块，将输入限制为 0 或 1。Simulink Design Verifier 搜索 20 个或更少时间步长的违规行为。由于该属性在假设下是有效的，因此无法发现违规行为。

open_system('sldvdemo_debounce_assumeblk');