HermesBDD

HermesBDD is a novel multi-core and multi-platform binary decision diagrams package focused on high performance and usability. HermesBDD supports a static and dynamic memory management mechanism, the possibility to exploit lock-free hash tables, and a simple parallel implementation of the ITE procedure based on a higher-level wrapper for threads and futures.

HermesBDD is completely written in C++ with no need to rely on external libraries and is developed according to software engineering principles such as testability, code coverage, and continuous integration to offer high usability, reliability, and easy maintenance over time.

The main repository of HermesBDD is at https://github.com/luigicapogrosso/HermesBDD. The software files in this repository are provided under the MIT License.

Introduction

There are several implementations of BDDs packages in the literature, but they focus mainly on package performance in terms of speedup and memory efficiency. However, we believe that performance is only one aspect on which to judge a BDD package. Other aspects matter too, such as (not necessarily in order of importance) functionality, robustness, reliability, portability, and documentation.

According to those principle, we developed HermesBDD: a novel multi-core and multi-platform binary decision diagram package focused on high performance and usability.

In summary, the contributions of HermesBDD are as follows:

  • Computationally faster, by exploiting multi-threading for parallel processing and concurrent access to a BDD;

  • Multi-platform (Windows, Linux, and macOS) to accommodate integration within tools from different environments;

  • Support for a static and dynamic memory management mechanism, the possibility to exploit lock-free hash tables, and a novel parallel implementation of the ITE procedure based on a higher-level wrapper for threads and futures;

  • High usability and robustness by design, thanks to development based on engineering principles such as code coverage and continuous integration, along with independence from external software.

Contribution guidelines

HermesBDD is not yet feature-complete, and there are still many interesting things left for you to do. So, this project welcomes contributions and suggestions. If you would like to contribute to HermesBDD, or do an internship or thesis, please contact the authors.

Installation

A pre-packaged source zip/tar.gz archive is always available in the releases section of HermesBDD’s GitHub space. Still, it is usually preferable to clone the repository using Git, in order to keep the distribution updated as soon as a new release is available. To do that, you shall issue:

$ git clone https://github.com/luigicapogrosso/HermesBDD.git

which creates the HermesBDD/ directory under the present working directory. Let’s switch into that directory.

Dependencies

HermesBDD has the following dependencies:

  • CMake, for compiling;

  • Sphinx, for documentation generation.

For further information about CMake and Sphinx, check the following 1 and 2 documentation page, respectively.

Building

The library is tested for compilation using GCC (minimum required: 10.2), Clang (minimum required: 11.0), and MSVC (minimum required: 19.20). The build system used is CMake. To build the library from sources in a clean way, it is preferable that you set up a build subdirectory, say:

$ mkdir build && cd build

Then, you can prepare the build environment, choosing a Release build for maximum performance:

$ cmake .. -DCMAKE_BUILD_TYPE=Release

At this point, if no error arises, you can build with:

$ cmake --build .

To install the library globally from built sources, you must do:

$ cmake --build . --target install

using sudo if you require administrator privileges for a Linux installation. Please note that the installation will build the whole distribution beforehand, hence it is preferable that you first build the other targets without administrator privileges, and build the install target.

CMake options

Available options are:

Option

Description

Default Value

NO_CACHE

Do not use cache

OFF

NO_THREAD

Do not use thread

OFF

NO_DYNMEM

Do not use dynamic memory allocation

OFF

COVERAGE

Enable coverage reporting

OFF

Introduction by Example

To import the library, add the following line to your file:

#include <hermesbdd.h>

Using HermesBDD

A simple use of the library is shown below:

#include <cassert>
#include <hermesbdd.h>

int main()
{
    // The True terminal.
    BDD one = BDD::bdd_true;
    // The False terminal.
    BDD zero = BDD::bdd_false;

    // Create a BDD variable x_0.
    BDD a(0);
    // Create a BDD variable x_1.
    BDD b(1);

    // Compute !a and check if !!a is really a.
    BDD not_a = !a;
    assert((!not_a) == a);

    // Compute a & b and !(!a ^ !b) and check if they are equivalent.
    BDD a_and_b = a & b;
    BDD not_not_a_or_not_b = !((!a) | (!b));
    assert(a_and_b == not_not_a_or_not_b);

    // Compute !BDD(1) and nithvar(1) and check if they are equivalent.
    BDD c(1);
    BDD not_c = !c;

    BDD d;
    d = d.nithvar(1);
    assert(not_c == d);

    return 0;
}

Package Reference

To create new BDDs, you can use:

  • BDD(v) : representation of literal ‘<v>’.

  • BDD nithvar(v) : representation of the negation of literal ‘<v>’.

  • BDD(node, dummy) : ‘<bdd>’ constructor that does not require creation of a node.

  • BDD::bdd_true : representation of constant ‘true’.

  • BDD::bdd_false : representation of constant ‘false’.

The following basic BDD operations are implemented:

  • bdd_a == bdd_b : compute ‘<bdd_a> == <bdd_b>’.

  • !bdd_a : compute the negation of <bdd_a>.

  • bdd_a & bdd_b : compute ‘<bdd_a> and <bdd_b>’.

  • bdd_a &= bdd_b : compute ‘<bdd_a> and eq. <bdd_b>’.

  • bdd_a | bdd_b : compute ‘<bdd_a> or <bdd_b>’.

  • bdd_a |= bdd_b : compute ‘<bdd_a> or eq. <bdd_b>’.

  • bdd_a ^ bdd_b : compute ‘<bdd_a> xor <bdd_b>’.

  • bdd_a ^= bdd_b : compute ‘<bdd_a> xor eq. <bdd_b>’.

  • bdd_a > bdd_b : compute ‘<bdd_a> then <bdd_b>’.

  • bdd_a >= bdd_b : compute ‘<bdd_a> then eq. <bdd_b>’.

  • bdd_a < bdd_b : compute ‘<bdd_b> then <bdd_a>’.

  • bdd_a <= bdd_b : compute ‘<bdd_b> then eq. <bdd_a>’.

  • ITE(A, B, C) : compute ‘if <A> then <B> else <C>’ with cache support.

  • ITE_without_cache(A, B, C) : compute ‘if <A> then <B> else <C>’ without cache support.

Authors