去抖时序属性

打开脚本

此示例说明如何使用 Simulink® Design Verifier™ Temporal Operator 模块对属性证明和测试用例生成的时序系统需求进行建模。

时序运算符

Simulink® Design Verifier™ 库提供了三个基本的时序运算符模块，可用于对时序属性进行建模。这些时序运算符旨在支持时序需求的设定，使建模的属性与实际的文本需求具有更紧密的关联性。这些模块是用于构造更复杂时序属性的低层构建模块。

去抖模型和需求

假设有一个去抖逻辑，该逻辑基于输入在固定时间步数内保持某个值，在值 0 和 1 之间进行去抖。

去抖功能在包含的 Stateflow® 图中捕获。

open_system('sldvdemo_debounce_to')
open_system('sldvdemo_debounce_to/debounce')

假设您要验证的去抖模型有两个需求。

需求 1：

每当输入等于 1 且持续超过 6 步时，输出应等于 2。

需求 2：

每当输出为 2 后输入变为 0 超过 5 步时，只要输入保持为 0，输出就应等于 1。

属性设定

要设定需求 1，您首先要表示输入等于 1 且持续超过 6 步的约束。这可以通过 Temporal Operator 模块库中的 Detector 模块来捕获。当检测到输入值为 1 且持续 7 个（或超过 6 个）时间步时，您需要检查是否只要检测后输入保持等于 1，输出就等于 2。使用 Detector 模块的“同步”选项，然后使用 Implies 模块，以捕获此约束。

open_system('sldvdemo_debounce_to/Verify True Output1')

可以组合多个时序运算符模块，以构造更复杂的时序属性。考虑需求 2。

open_system('sldvdemo_debounce_to/Verify True Output2')

为了便于说明，将此需求大致分解为三个关注点：

  1. 输出为 2 后：这是属性的启用条件。在检查其余约束时，您需要知道此条件在过去的某个时间点是否为 true。这种类型的启用条件通常后跟一个延长器（“有限”或“无限”），它与其他约束条件组合，可能构成蕴涵逻辑的第一个输入。

  2. 输入变为 0 且持续超过 5 步，只要输入保持为 0，就进行检查：出于与第一个属性相同的原因，您使用具有“同步”输出（“输入检测时间步数”= 6）的 Detector。

  3. 输出应等于 1：这是当前两个约束成立时您要验证的条件。这可以通过逻辑 Implies 模块来捕获。请注意，这里不能使用 Within Implies 模块。

属性证明

对时序需求进行建模后，您可以使用 Simulink Design Verifier 对这些需求执行属性验证。

清理

要完成示例，请关闭所有打开的模型。

close_system('sldvdemo_TOBlocks',0);
close_system('sldvdemo_debounce_to',0);