DSVerifier - Digital Systems Verifier
Clone or download
Pull request Compare This branch is 732 commits ahead, 3 commits behind hussamaa:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
benchmarks
bmc
gui
regression
scripts
src
toolbox-dssynth
toolbox-dsvalidator
toolbox-dsverifier
utils
.gitignore
.project
.travis.yml
LICENSE.md
README.md
makefile

README.md

Build Status

DSVerifier (Digital-Systems Verifier)

DSVerifier is a verification tool for digital systems. In particular, DSVerifier employs bounded model checking (BMC) techniques based on satisfiability modulo theories (SMT) and boolean satisfiability (SAT), which allows engineers to verify the occurrence of design errors, due to the finite word-length (FWL) effects employed in fixed-point digital filters and controllers.

Supported properties:

For Digital-Systems:
  • Overflow
  • Limit Cycle
  • Timing
  • Error
  • Stability
  • Minimum Phase
  • Settling time
  • Overshoot
For Digital-Systems in Closed-loop:
  • Stability
  • Limit Cycle
  • Quantization Error
  • Settling time
  • Overshoot

Configuration

(1) Before using DSVerifier, we need to configure an environment variable called DSVERIFIER_HOME. You should add it to your .bashrc file as follows:

 export DSVERIFIER_HOME='path to dsverifier folder'

After that, you should save it and use the following command:

 $ source .bashrc

(2) You should download the (desired) version of CBMC or ESBMC executables for DSVerifier. This package contains CBMC v5.6 and ESBMC v4.0. Please, add them to $DSVERIFIER_HOME/model-checker

CBMC and ESBMC recommended versions for DSVerifier v2.0.3 are:

(3) You need to install the Eigen library (e.g., eigen3, eigen3-static, and eigen3-devel depending on your distribution).

(4) Make sure that you have installed GCC version 5.4 (or higher).

Command line mode

Verification of Digital-Systems

It is necessary to generate a verification file using the following format:

#include <dsverifier.h>

digital_system ds = {
  .a = { 1.0, 1.068, 0.1239 },
  .a_size = 3,
  .b = { 2.813, -0.0163, -1.872 },
  .b_size = 3
};

implementation impl = {
  .int_bits = 4,
  .frac_bits = 10,
  .min = -5.0,
  .max = 5.0
};

Execution:

  ./dsverifier ds.c --realization <r> --property <j> --x-size <k>

where ds.c is the digital-system specification file, r is the chosen realization, j is the property to be verified, and k is the verification bound.

  • Properties: OVERFLOW, LIMIT_CYCLE, ZERO_INPUT_LIMIT_CYCLE, TIMING, ERROR, STABILITY, and MINIMUM_PHASE.
  • Realizations: DFI, DFII, TDFII, DDFI, DDFII, and TDDFII.
Verification of Digital-Systems in Closed-loop

It is necessary to generate a verification file using the following format:

#include <dsverifier.h>

digital_system plant = {
  .b = { 0.00018604, 0.000172886972 },
  .b_uncertainty = { 5, 5 },
  .b_size = 2,
  .a = { 1.0,-1.7989, 0.80248974 },
  .a_uncertainty = { 5, 5, 5 },
  .a_size = 3
};

digital_system controller = {
  .b = { 1.422, -1.1360358, -1.41689538972, 1.14114041028 },
  .b_size = 4,
  .a = { 1.0, -1.0307, -0.861428, 0.892128 },
  .a_size = 4
};

implementation impl = {
  .int_bits = 16,
  .frac_bits = 12,
  .min = -1.0,
  .max = 1.0,
  .max_error = 5
};

Execution:

  ./dsverifier <file> --connection-mode <cm> --property <j>
                      --realization <r> --x-size <k> --bmc CBMC

where file is the digital-system specification file, cm is the chosen connection-mode, j is the property to be verified, r is the desired realization, and k is the verification bound.

  • Connection mode: SERIES and FEEDBACK

  • Properties: STABILITY_CLOSED_LOOP, LIMIT_CYCLE_CLOSED_LOOP, and QUANTIZATION_ERROR_CLOSED_LOOP

  • Realizations: DFI, DFII, and TDFII.

Graphical User Interface

To use DSVerifier GUI, it is necessary to have at least Java Runtime Environment Version 8.0 Update 40 (jre1.8.0_40)

Execution:

 java -jar dsverifier-gui.jar