Table of Contents
This is a minimal Reduced Ordered Binary Decision Diagram (ROBDD) package written in C++. This package implements the fundamental manipulation methods for BDDs as they were introduced in the lecture Verification of Digital Systems by Prof. Kunz. The package was implemented using the Test Driven Development paradigm presented by Dr. Wedler.
The project is split into three parts.
-
Implementation of the basic functionality of the BDD package using the TDD methodology. This is the biggest part of the project.
-
Improvement of the performance of the implementation via provided benchmarks.
-
Extending the existing implementation by a practical application of BDD. Using BDDs, it is possible to symbolically represent a state-space and perform a reachability analysis.
List of dependencies required to compile the project:
- Boost 1.81 or higher (
libboost-all-dev) - Graphviz (
graphviz-dev) - GoogleTest (
libgtest-dev)
Be aware that this project uses boost::unordered_flat_map and thus requires Boost 1.81 or higher, which is not currently available in Ubuntu's official repository. If you don't have access to this version of the library, you can use boost::unordered_map with minor adjustments.
-
Install the dependencies
-
Clone the repo
git clone https://github.com/rpigor/librobdd
Installation with CLion
CLion comes with CMake.
-
Open CLion and open librobdd/CMakeLists.txt as a project
-
Select your target and build the project
Installation without CLion
- Navigate to the project folder
cd librobdd - Invoke CMake to create the build directory and generate makefiles
cmake -S . -B build - Invoke CMake to build the project
cmake --build build
Thank you Veli Durmuşcan, Shreya Vithal Kulhalli and Osama Omar Youssif Ayoub for the work on this README.md.