Symbolic Execution and Simulation with AADD

This page gives a brief introduction into Affine Arithmetic Decision Diagrams, short AADD. AADD enable the efficient and scalable symbolic execution of many programs, e.g.

  • Signal processing systems and embedded software, and
  • Analog/digital systems at block diagram level.

The model or software must be written in Java, Kotlin with jAADD, or C++ and SystemC models with the  older libAADD. Basis for this is the use of Affine Arithmetic Decision Diagrams, short: AADD. An introduction of the underlying concept can be found here. The software can be downloaded under github.com/TUK-CPS.

What can I do with AADD?

AADD permit the efficient representation and tracing of uncertainties in mixed discrete/continuous computations. Examples are algorithms with real-valued computations and some control flow that depends on the results of the computations. A typical use case is symbolic execution of signal processing methods in C++ and/or Java or Kotlin. As a simple example, the following program can be executed symbolically with AADD (example in C++ V2.0):

#include "aadd.h" 

 

doubleS a;  // Data types with S are computed symbolically.

 

int main()

{

    a = doubleS(0,100); // a takes double value from range [0,100]

   

    ifS(a > 1)          // symbolic cond. and iteration statements

    a = a + 2;

    elseS

    a = a - 2;

    endS;

   

    cout << "a is: " << endl;

    cout << a;

 

}

The result of symbolic execution is a decision diagram that represent all possible results, assuming that a is from the range [0,100]: The condition at the root node is (a>1), and the leaf nodes have the ranges [-2,98] and [2,102], depending on the condition. Ranges are represented and computed by affine forms to yield scalability. Note that by considering the condition, these ranges can be further reduced significantly to [-2,-1] and [3,102]. This is done by an LP solver (GLPK for C++, Apache Math for Java/Kotlin) that improves accuracy of the affine forms, while maintaining scalability.

If AADD are used in a simulator such as SystemC (TLM, AMS), this permits symbolic simulation. The result is then a sequence of AADD that represent all possible trajectories of output signals. As AADD are accurate and scale very well for systems that are mostly linear, it is particular well suited for symbolic simulation of analog/mixed-signal (AMS) systems.  

Versions and installation

There are two versions of AADD:

  1. The "new" jAADD version, which provides a library for use on the Java Virtual Machine.
  2. The "older" libAADD version, which provides a library for use with C++, SystemC, C, etc.

We strongly recomment the use of the jAADD library which is significantly more advanced.We plan to provide a binary-version of this library which then will replace the libAADD version.

For installation and an instruction, we refer to the documentation in the Github.