Documentation

–
Download the lastest version of DSVerifier at download page.
A video demonstration is available at:    [Demonstration]
The source code is available at:   https://github.com/ssvlab/dsverifier

Command Line Version

1) Generate manually a .c file with system specification.

For Digital-Systems standalone verification

#include <dsverifier.h>

digital_system ds = {
    .a = { 1.0, -0.9 },               /* digital system denominator coefficients */
    .a_size = 2,                      /* number of coefficients in denominator */   
    .b = { 1.561, -1.485 },           /* digital system numerator coefficients */
    .b_size = 2                       /* number of coefficients in numerator */   
 }; 

implementation impl = {
    .int_bits = 3,                    /* number of bits in integer part of the fixed-point representation */
    .frac_bits = 8,                   /* number of bits in precision part of the fixed-point representation */
    .delta = 0.25,                    /* delta value used for delta form (if any) */
    .max = 1.0,                       /* maximum value used in the digital system input */
    .min = -1.0,                      /* minimum value used in the digital system input */
 };

DSVerifier must be invoked using the following parameters:

./dsverifier example.c --realization DFI --property OVERFLOW --x-size 10 --bmc ESBMC --solver z3

For Digital-Systems in Closed-loop considering uncertainty

#include <dsverifier.h>

digital_system plant = {
   .b = { 0.5486931, -0.886738 },     /* sampled plant numerator coefficients */
   .b_uncertainty = { 0, 0 },         /* uncertainty numerator coefficients */
   .b_size = 2,                       /* number of coefficients in numerator */
   .a = { 1.0, -3.324812, 1.648721 }, /* sampled plant denominator coefficients */
   .a_uncertainty = { 0, 0, 0 },      /* uncertainty numerator coefficients */
   .a_size = 3                        /* number of coefficients in denominator */
};

digital_system controller = {            
   .b = { -18.791301, 11.383944 },    /* digital control numerator coefficients */
   .b_size = 2,                       /* number of coefficients in numerator */   
   .a = { 1.0, 3.635450 },            /* digital control denominator coefficients */
   .a_size = 2                        /* number of coefficients in denominator */   
};

implementation impl = {
    .int_bits = 3,                      /* integer part of the fxp representation (for controller) */
    .frac_bits = 8,                   /* precision part of the fxp representation (for controller) */
 };

DSVerifier must be invoked using the following parameters:

./dsverifier example2.c --property STABILITY_CLOSED_LOOP --connection-mode SERIES --bmc ESBMC --solver z3

2) Inspect the verification result:

VERIFICATION SUCCESSFUL ~ There is no violation of the property (i.e., the digital system specification meets its implementation)