–

**DSValidator** is an automated counterexample reproducibility tool based on MATLAB with the goal of reproducing counterexamples generated by the DSVerifier tool that refute specific properties related to digital systems.

**Useful links:**

Download the lastest version of DSValidator Toolbox at download page.

Video demonstration about DSValidator Toolbox Installation at: [Install Demonstration]

Video demonstration about DSValidator Toolbox Usage at: [Usage Demonstration]

See details about the functions available at DSValidator Toolbox in documentation page.

## Prerequisites:

In order to execute DSValidator in MATLAB, the user must install the DSValidator tool in MATLAB 2016b Linux version.

Each counterexample must be stored as a “.out” file extension. If the user has more than one digital system to be validated, a directory with all “.out” files must be created.

Required tools to run the scripts: **Linux/MATLAB**;

MATLAB version: at least version **2016b**;

## Installation:

In order to install DSValidator, the user must download the DSValidator installation file from the DSVerifier web page.

After that, the following steps should be executed:

1. Open MATLAB;

2. Execute the file with the “$.mltbx$” extension (or double-click on it); a pop-up screen to install DSValidator will be shown.

3. Click on the **install** button.

## Toolbox Features

**How can a user generate ‘.out’ file in DSVerifier?**

Run DSVerifier via command-line using “**– -show-ce-data**”, which is a required parameter to correctly execute and use DSValidator.

See details how to run DSVerifier in documentation page.

**Running the Automatic Validation **

Invoke the function ‘validation’:

>> validation(path, property, ovmode, rmode, filename);

The **path** is the directory with all counterexamples and **property** is defined as:

- ‘m’: for Minimum Phase Validation;
- ‘s’: for Stability Validation;
- ‘o’: for Overflow Validation;
- ‘lc’: for Limit Cycle Validation.

The **vmode** is the overflow mode; possible values can be:

- ‘saturate’ for saturate overflow
- ‘wrap’ for wrap around overflow

The **rmode** is the rounding mode; possible values can be:

- ’round’ to use round as rounded mode
- ‘floor’ to use floor as rounded mode

The **filename**: the name of .MAT file generated as result from validation. By default, the value is ‘digital_system’.

The **.MAT File** has the counterexamples extracted in the following structure:

**MATLAB Results:**

After you run the automatic validation, a .MAT file is generated with all counterexamples extracted and their results from validation: Reproducible or Irreproducible.

**Reproducible**: this means that the counterexample is reproducible.

**Irreproducible**: the reproducibility performed by MATLAB has a different result of DSVerifier.

You can check the counterexamples stored in the .MAT file, that is implemented and organized as a group of structs with information about the digital system, implementation, inputs, outputs, realization, word length, dynamical range, and sample time.

In addition, after executing **validation**, the validation result prints statistics about each counterexample (or test case).

**MATLAB Functions:**

** Macro Functions **

Represent functions to reproduce the validation steps (e.g., extraction, parser, simulation, comparison, and report).

** Validation Functions **

Check and validate the violated property (e.g., overflow, limit cycle, stability, and minimum phase).

** Realization Functions **

Reproduce realizations for the delta/direct form I, II, and transposed direct form II.

** Numerical Functions **

Perform the quantization process, rounding mode, overflow mode (wrap-around and saturate), fixed-point operations as sum, subtraction, multiplication, division, and delta operator.

** Graph Functions **

Plot the graphical representation of overflow, limit cycle oscillations, and poles/zeros representing stability/minimum phase with or without FWL effects inside a unitary circle.

See details about the functions available at Toolbox in functions documentation page.

## Toolbox Usage

1) **Generate manually a .c file** with system specification. Consider an example of a digital system description in the following ANSI-C file:

#include <dsverifier.h> digital_system ds = { .b = { 2002.0, -4000.0, 1998.0 }, .b_size = 3, .a = { 1.0, 0.0, -1.0 }, .a_size = 3, .sample_time = 0.001 }; implementation impl = { .int_bits = 13, .frac_bits = 3, .max = 1.0, .min = -1.0 };

2) **Execute DSVerifier**. The **DSVerifier** verification must be invoked in command line using the following parameters:

./dsverifier input.c --realization DFI --property LIMIT_CYCLE --x-size 10 --bmc CBMC --show-ce-data > dsv_limit_system_02.out

A **counterexample** will be printed as a .out file as follows:

VERIFICATION FAILEDCounterexample Data: 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 Dynamic Range = {-1,1} Initial States = { -0.875 0.0 -1.0 } 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 }

3) **Execute the automatic validation**. In **MATLAB Workspace**, considering that the toolbox is already installed, you can invoke in command line the following function:

validation('/home/user/counterexample','lc','wrap','round','ce_limit');

* The path should contain the .out files.

The **result** of the automated counterexample validation for this particular example is:

Counterexamples Validation Report...CE 1 time: 0.11177 status: reproducible General Report: Total Counterexamples Reproducible: 1 Total Counterexamples Irreproducible: 0 Total Counterexamples: 1 Total Time Execution: 0.11177

And a **.MAT file** named ‘ce_limit’ is generated in your MATLAB workspace.

Videos with previous version playlist .

Controllers/Counterexamples used in videos: download files.