DSVerifier Toolbox Documentation

Back-end Functions:
Value Description
verificationSetup Setup the DSVERIFIER_HOME and model checkers visibility (ESBMC or CBMC) in a variable environment
verificationParser Reads the system in MATLAB form and translate to a ANSI-C file
verificationExecution Function to get the parameters, system and implementation to start the verification
verificationReport Shows the report about the verification: successful or failed, and generate the counterexample in .MAT format.
Verification Functions - Transfer-Function for Open-Loop Systems:
Value Description
verifyOverflow(system, intBits, fracBits, rangeMax, rangeMin, realization, kbound) Checks overflow property violation for digital systems using a bounded model checking tool.
verifyError(system, intBits, fracBits, rangeMax, rangeMin, realization, error, kbound) Checks quantization error property violation for digital systems using a bounded model checking tool.
verifyLimitCycle(system, intBits, fracBits, rangeMax, rangeMin, realization, kbound) Checks limit cycle property violation for digital systems using a bounded model checking tool.
verifyMinimumPhase(system, intBits, fracBits, rangeMax, rangeMin, realization) Checks minimum phase property violation for digital systems using a bounded model checking tool.
verifyStability(system, intBits, fracBits, rangeMax, rangeMin, realization) fChecks stability property violation for digital systems using a bounded model checking tool.
Verification Functions - Transfer-Function for Closed-Loop Systems:
Value Description
verifyClosedStability(controller, plant, intBits, fracBits, rangeMax, rangeMin, connectionMode) Checks stability property violation for closed-loop digital systems using a bounded model checking tool.
verifyClosedLoopLimitCycle(controller, plant, intBits, fracBits, rangeMax, rangeMin, realization, kbound, connectionMode) Checks limit cycle property violation for closed-loop digital systems using a bounded model checking tool.
verifyClosedLoopQuantizationError(controller, plant, intBits, fracBits, rangeMax, rangeMin, realization, kbound, connectionMode) Checks quantization error property violation for closed-loop digital systems using a bounded model checking tool.
Verification Functions - State-Space for Open-Loop Systems:
Value Description
verifyStateSpaceControllability(system, inputs, intBits, fracBits, rangeMax, rangeMin) Checks controllability property violation for digital systems (state-space representation) using a bounded model checking tool.
verifyStateSpaceObservability(system, inputs, intBits, fracBits, rangeMax, rangeMin) Checks observability property violation for digital systems (state-space representation) using a bounded model checking tool.
verifyStateSpaceQuantizationError(system, inputs, intBits, fracBits, rangeMax, rangeMin, errorLimit) Checks quantization error property violation for digital systems (state-space representation) using a bounded model checking tool.
verifyStateSpaceStability(system, inputs, intBits, fracBits, rangeMax, rangeMin) Checks stability property violation for digital systems (state-space representation) using a bounded model checking tool.
Verification Functions - State-Space for Closed-Loop Systems:
Value Description
verifyStateSpaceControllability(system, inputs, intBits, fracBits, rangeMax, rangeMin, K) Checks controllability property violation for digital systems (state-space representation) using a bounded model checking tool.
verifyStateSpaceObservability(system, inputs, intBits, fracBits, rangeMax, rangeMin, K) Checks observability property violation for digital systems (state-space representation) using a bounded model checking tool.
verifyStateSpaceQuantizationError(system, inputs, intBits, fracBits, rangeMax, rangeMin, errorLimit, kbound, K) Checks quantization error property violation for digital systems (state-space representation) using a bounded model checking tool.
verifyStateSpaceStability(system, inputs, intBits, fracBits, rangeMax, rangeMin, K) Checks stability property violation for digital systems (state-space representation) using a bounded model checking tool.

Parameters from the functions:

  • system: digital-system represented in transfer-function or state-space format;
  • intBits: number of integer bits;
  • fracBits: number of fractional bits;
  • rangeMax: the maximum dynamical range;
  • rangeMin: the minimum dynamical range;
  • kbound: the k-bound to be employed during the verification;
  • realization: the realization form (delta or direct -forms); delta-forms: DDFI, DDFII and TDDFII; direct-forms: DFI, DFII and TDFII;
  • error: the maximum error for quantization-error verification;
  • controller: for closed-loop verification, the controller is represented by tranfer-function format;
  • plant: for closed-loop verification, the plant is represented by tranfer-function format;
  • connectionMode: the connection mode for closed-loop verification; the value must be ‘series’ or ‘feedback';
  • inputs: the inputs matrix used verification for state-space systems;
  • K: the feedback matrix used in closed-loop verification for state-space systems;