Main Content

Debounce Temporal Properties

Open Script

This example shows how to model temporal system requirements for property proving and test case generation using Simulink® Design Verifier™ Temporal Operator blocks.

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')

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')

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

open_system('sldvdemo_debounce_to/Verify True Output2')

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

  1. 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.

  2. 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).

  3. 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);