In order to use all functions presented in this documentation, you should download DSValidator from the download page.

Follow the instructions to install the toolbox according to the install page.

## Proposed Counterexample Format

**DSValidator** exploits counterexamples provided by the DSVerifier tool. In particular, if there is a property violation, then DSVerifier shows a counterexample, which contains inputs and states that lead the digital system to the failure state.

Given the digital system represented by the transfer-function in MATLAB:

system = tf([2002 -4000 1998],[1 0 -1]);

The code bellow shows an example of the present counterexample format related to a overflow limit-cycle violation for the previous digital system described in transfer-function:

Property = LIMIT_CYCLE Numerator = { 2002, -4000, 1998 } Denominator = { 1, 0, -1 } X_Size = 10 Sample_Time = 0.001 Implementation = <13,3> Numerator (fixed-point) = { 2002, -4000, 1998 } Denominator (fixed-point) = { 1, 0, -1 } Realization = DFI Dynamical_Range = { -1, 1 } Initial_States = { -0.875, 0, -1 } Inputs = { 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5} Outputs = { 0, -1, 0, -1, 0, -1, 0, -1, 0, -1}

## Producing The Counterexample

In DSVerifier, users must provide a specification that contains the digital system numerator and denominator coefficients (resp. “b” and “a”); the implementation specification that contains the number of bits in the integer and fractional parts (resp. “int_bits” and “frac_bits”); and the input range (“max” and “min”). For delta realizations, user must also provide the delta operator (“delta”). In the command-line version, DSVerifier can be invoked as:

dsverifierinput.c--realizationi--propertyj--x-sizek--BMCbmc--show-ce-data > file.out

where **input.c** is the digital system specification file, **i** is the chosen realization form, **j** is the property to be verified, **k** is the verification bound, i.e., the number of times that the digital system is unwound, while the parameter **bmc** indicates the BMC tool to be used ESBMC or CBMC. DSVerifier supports four different properties: OVERFLOW, LIMIT_CYCLE, STABILITY, and MINIMUM_PHASE. The code bellow shows a specification file example with one digital system and one implementation, where “b_size” and “a_size” represent the number of coefficients in the numerator and denominator, respectively.

#include "dsverifier.h" digital_system ds = { .b = { 1.5, -0.5 }, .b_size = 2, .a = { 1.0, 0.0 }, .a_size = 2, .sample_time = 0.02 }; implementation impl = { .int_bits = 2, .frac_bits = 14, .max = 1.0, .min = -1.0, };

Using the specification in defined in the code above as an input.c file, DSVerifier can be invoked to check a specific property. The parameter –show-ce-data must be added to ensure that the counterexample is provided in a “.out” file. In our example, the goal is to check an overflow violation, which considers the digital system for DFI realization and a numerical format {2,14}. DSVerifer is invoked as:

dsverifier input.c --realization DFI --property OVERFLOW --x-size 10 --BMC CBMC --show-ce-data > ds1_impl1_DFI.out

Now, the user has an output file that is generated with the respective counterexample for the overflow property (ds1_impl1_DFI.out).

If the user opens the ds1_impl1_DFI.out file, then the counterexample is shown bellow:

VERIFICATION FAILED Counterexample Data: Property = OVERFLOW Numerator = { 0.1, -0.09996 } Denominator = { 1.0, -1.0 } X Size = 10 Sample Time = 0.02 Implementation = <10,6> Numerator (fixed-point) = { 384.0, -128.0 } Denominator (fixed-point) = { 256.0, 0.0 } Realization = DFI Dynamic Range = {-1,1} Inputs = { 85.328125, -0.0625, 0.0, -128.6875, -215.984375, -256.0, 256.0, -197.359375, 0.0 85.34375 } Outputs = { 128.0, -42.765625, 0.03125, -193.03125, -259.640625, -276.0, 512.0, -424.046875, 98.6875, 128.015625 }

## Functions Description

The struct ‘system’ used in many functions implemented in DSValidator should have the following features:

Attribute | Description |
---|---|

system.sys.a |
represents the denominator; |

system.sys.b |
represents the numerator; |

system.sys.tf |
represents the transfer function system representation |

system.impl.frac_bits |
represents the fractionary bits |

system.impl.int_bits |
represents the integer bits |

system.impl.realization_form |
represents the realization, and it should be DFI, DFII, TDFII, DDFI, DDFII or TDDFII |

system.inputs.const_inputs |
represents the inputs from counterexample |

system.inputs.initial_states |
represents the initial states from counterexample |

system.outputs.output_verification |
represents the output extracted from counterexample |

system.impl.delta |
represents in delta form realizations, the delta operator that should be informed |

system.impl.sample_time |
represents the sample time of realization |

system.impl.x_size |
represents the bound size |

Value | Description |
---|---|

(m) |
for minimum phase |

(s) |
for stability |

(o) |
for overflow |

(lc) |
for limit cycle. |

Function | Description |
---|---|

validationExtraction(directory, p) |
Function to extract all counterexamples from .out files generated by DSVerifier. Where 'directory' should be the path with all counterexamples inside .out files. The parameter 'p' is the property to be analyzed. |

validationParser(p) |
Script to get the counterexamples parameters and transform them in variables on workspace, where 'p' is the property to be analyzed. The function validationExtraction must be done before this function! |

validationSimulation(system, p) |
Script to simulate and validate a property for a system automatically. |

validationComparison(system, p) |
Script to verify and compare the results between MATLAB and DSVerifier. |

validationReport(digital_system) |
Script to generate a report about automatic validation. |

validation(path, property, ovmode, rmode, filename) |
Script to run all steps to validate counterexamples. |

Function | Description |
---|---|

reproduceLimitCycle(path) |
Script developed to reproduce limit cycle property given a 'path' with all .out counterexamples. |

reproduceOverflow(path) |
Script developed to reproduce overflow property given a 'path' with all .out counterexamples. |

reproduceMinimumPhase(path) |
Script developed to reproduce minimum phase property given a 'path' with all .out counterexamples. |

reproduceStability(path) |
Script developed to reproduce stability property given a 'path' with all .out counterexamples. |

Function | Description |
---|---|

simulate_limit_cycle(system) |
Script developed to reproduce the limit cycle counterexamples using DFI, DFII and TDFII realizations. |

simulate_overflow(system) |
Script developed to reproduce the overflow property in counterexamples. Give the system as a struct with all parameters of counterexample then matlab will check overflow property for direct and delta forms. |

simulate_minimum_phase(system) |
Script developed to reproduce the minimum phase property in counterexamples. Give the system as a struct with all parameters of counterexample then matlab will check minimum phase property for direct and delta forms. |

simulate_stability(system) |
Script developed to reproduce the stability property in counterexamples. Give the system as a struct with all parameters of counterexample then matlab will check stability property for delta and direct forms. |

Function | Description |
---|---|

realizationDF1(system) |
Simulate and reproduce a counterexample for limit cycle using DFI realization. In case of delta form (DDFI), the delta operator should be represented in system struct. |

realizationDF2(system) |
Simulate and reproduce a counterexample for limit cycle using DFII realization. In case of delta form (DDFII), the delta operator should be represented in system struct. |

realizationTDF2(system) |
Simulate and reproduce a counterexample for limit cycle using TDFII realization. In case of delta form (TDDFII), the delta operator should be represented in system struct. |

Function | Description |
---|---|

deltapoly(b,a,delta) |
Performs the delta transformation for a transfer function b(z)/a(z). Where a is the denominator polynomial, b is the numerator polynomial and delta is transformation step factor. |

fxp_add(aadd, badd, wl) |
Function to perform a fixed point addition out = a + b; Where: aadd is fixed point input, badd is fixed point input and wl is fractional word lenght. |

fxp_div(adiv,bdiv, wl) |
Function to perform a fixed point division out = a / b; Where: adiv is fixed point input, bdiv is fixed point input and wl is fractional word lenght. |

fxp_mult(amult, bmult, wl) |
Function to perform a fixed point multiplication out = amult * bmult; Where: amult is fixed point input, bmult is fixed point input and wl is fractional word lenght. |

fxp_sub(asub, bsub, wl) |
Function to perform a fixed point subtraction out = a – b; Where: asub is fixed point input, bsub is fixed point input and wl is fractional word lenght. |

fxp_quantize (num, wl) |
Function to perform a fixed point quantization function; Where: num is a input value to be quantized and wl is fractional word lenght. This function considers the round and floor rounding mode. |

mode_saturate(value, n, l) |
Function to saturate mode for arithmetic overflow. Where, 'value' is number to be converted in case of arithmetic, 'n' is integer bits implementation and 'l' is fractionary bits implementation. |

mode_wrap(value, n, l) |
Function to wrap-around mode for arithmetic overflow. Where, 'value' is number to be converted in case of arithmetic, 'n' is integer bits implementation and 'l' is fractionary bits implementation. |

shiftL(zIn,z, nZ) |
The main objective of this function is flip the vector in the right-left direction and including a value in the end of vector in each interaction of the realization. Function developed to support the realizations (DFI,DFII and TDFII). zIn is the value to be shift, z is a vector to be interacted and nZ the size of z vector. |

shiftL(zIn,z, nZ) |
The main objective of this function is flip the vector in the left-right direction and including a value in the end of vector in each interaction of the realization. Function developed to support the realizations (DFI,DFII and TDFII). zIn is the value to be shift, z is a vector to be interacted and nZ the size of z vector. |

fwl(a,l) |
Obtains the FWL format of polynomial 'a' with 'l' fractional bits. |

Function | Description |
---|---|

plot_limit_cycle(system) |
Plot the limit cycle output of your system. Where system is a struct from a counterexample extracted (generated by .MAT file). |

plot_overflow(system) |
Plot the overflow output of your system. Where system is a struct from a counterexample extracted (generated by .MAT file). |

plot_zero_pole(system) |
Plot the poles and zeros of your system (very useful for stability and minimum phase) considering fwl effects. Where system is a struct from a counterexample extracted (generated by .MAT file). |