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

使用 Assumption 模块进行属性证明

打开脚本

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

open_system('sldvdemo_debounce_assumeblk');