DSValidator Documentation

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:

dsverifier input.c --realization i  --property j --x-size k --BMC bmc --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:

Template Struct for System:
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
Properties Available:
Value Description
(m) for minimum phase
(s) for stability
(o) for overflow
(lc) for limit cycle.
Macro Functions Description:
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.
Front-End Functions Description:
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.
Validation Functions Description:
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.
Realizations Functions Description:
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.
Numerical Functions Description:
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.
Graphical Functions Description:
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).