–
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 FAILED
Counterexample 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.