matlab debounce,Debounce Temporal Properties

matlab debounce,Debounce Temporal PropertiesTemporalOperatorsTheSimulink®DesignVerifier™libraryprovidesthreebasictemporaloperatorblockscanbeusedtomodeltemporalproperties.Theintentofthetemporaloperatorsistosupportthe…

大家好,又见面了,我是你们的朋友全栈君。

Temporal Operators

The Simulink® Design Verifier™ library provides three basic temporal operator blocks can be used to model temporal properties. The intent of the temporal operators is to support the specification of temporal requirements, such that the modeled property has a closer co-relation to the actual textual requirement. These blocks are low-level building blocks for constructing more complex temporal properties.

Debounce Model and Requirements

Consider a debounce logic that debounces between values of 0 and 1 based on the input holding a value for a fixed number of time steps.

The debounce functionality is captured in the containing Stateflow® chart.

open_system(‘sldvdemo_debounce_to’)

open_system(‘sldvdemo_debounce_to/debounce’)

56e4f0795cf35e4d8361ab78e9761491.png

Consider two requirements of the debounce model that you would like to verify.

Requirement 1:

Whenever the input equals 1 for more than 6 steps, the output shall be equal to 2.

Requirement 2:

Whenever the input becomes 0 for more than 5 steps after the output was 2, the output shall equal 1 as long as the input stays at 0.

Property Specification

For specifying Requirement 1, you first represent the constraint that input equals 1 for more than 6 steps. This can be captured by the Detector block from the Temporal Operator Blocks Library. On detecting that the input value is 1 for 7 (or more than 6) time steps, you want to check that the output equals 2 as long as input stays equal to 1 after the detection. Use the “Synchronized” option of the Detector block followed by an Implies block to capture this.

open_system(‘sldvdemo_debounce_to/Verify True Output1’)

831c63f08e426cd8f76a897c5ad4eb78.png

Multiple temporal operator blocks can be combined to construct more complex temporal properties. Consider Requirement 2.

open_system(‘sldvdemo_debounce_to/Verify True Output2’)

3d83642ce91a6ce889855e08445257b1.png

For illustration, this requirement is broken down roughly into three pieces of interest:

After the output was 2: This is an enabling condition for your property. While checking the rest of the constraints, you want to know if this condition was true at some point in the past. This type of an enabling condition is typically followed by an Extender (either “Finite” or “Infinite”) that, in combination with other constraints, might form the first input to your implication.

The input becomes 0 for more than 5 steps and check something as long as input stays 0: For the same reason as the first property, you use a Detector with “Synchronized” output (“Time steps for input detection” = 6).

The output shall equal 1: This is the condition that you want to verify whenever the first two constraints hold. This is captured through a logical Implies block. Note that you cannot use Within Implies block here.

Property Proving

Once the temporal requirements have been modeled, you can perform property proving on these using Simulink Design Verifier.

Clean Up

To complete the example, close all the opened models.

close_system(‘sldvdemo_TOBlocks’,0);

close_system(‘sldvdemo_debounce_to’,0);

版权声明:本文内容由互联网用户自发贡献,该文观点仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 举报,一经查实,本站将立刻删除。

发布者:全栈程序员-用户IM,转载请注明出处:https://javaforall.cn/151555.html原文链接:https://javaforall.cn

【正版授权,激活自己账号】: Jetbrains全家桶Ide使用,1年售后保障,每天仅需1毛

【官方授权 正版激活】: 官方授权 正版激活 支持Jetbrains家族下所有IDE 使用个人JB账号...

(0)
blank

相关推荐

发表回复

您的电子邮箱地址不会被公开。

关注全栈程序员社区公众号