GitHub repository for the Verification of Digital Systems Class Project
Report Bug
Table of Contents
In the course of this Lab assignment, students are going to implement a minimal BDD package in C++. This package implements the fundamental manipulation methods for ROBDDs as they were introduced in the lecture Verification of Digital Systems by Prof. Kunz. The package will be implemented using the Test Driven Development (TDD) 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.
Main tasks in this part:
- Set up and maintain a Git repository
- Use CMake as a build system of the project
- Verify the code using GTest
- Set up a Continuous Integration (CI) pipeline with GitHub Actions (Mandatory)
- Use Doxygen (or a similar tool) to generate documentation for the API. (Optional)
Improvement of the performance of the implementation via provided benchmarks.
Main tasks in this part:
- Learning how to identify performance bottlenecks within the code.
- Analyzing benchmark results.
- How to overcome bottlenecks.
Extending the existing implementation by a practical application of BDD. Using BDDs, it is possible to symbolically represent a state-space. This representation allows to check quickly, whether a specific state is within the reachable state space or not.
Fork this repository and follow the instructions given in doc/ to complete the project.
List of Ubuntu packages required to complete the project:
- git-all
- libboost-all-dev
- build-essential
No guarantee that this list is complete (Add other packages to the README)
- Clone the repo
git clone https://github.com/your_username_/VDSProject
Installation with CLion
CLion comes with CMake. 2. Open CLion and open VDSProject/CMakeLists.txt as a project. 3. Select your target and build the project.
Installation without CLion
- Navigate to the project folder and create a build directory
cd VDSProject && mkdir build
- Navigate to the build folder and invoke CMake
cd build && cmake ../
- Invoke make
make
Generated by doxygen in https://victorherbert.github.io/VDSProject/
- TODO
- DONE
| Function Name | Implemented | Tested | Person |
|---|---|---|---|
| OBDDManager() | [X] | [X] | Victor |
| OBDDManager(std::vector nodes) | [X] | [X] | Kamel |
| createVar(const std::string &label) | [X] | [X] | Victor |
| True() | [X] | [X] | Victor |
| False() | [X] | [X] | Victor |
| isConstant(BDD_ID f) | [X] | [X] | Victor |
| isVariable(BDD_ID x) | [X] | [X] | Victor |
| isExpression(BDD_ID x) | [X] | [X] | Victor |
| topVar(BDD_ID f) | [X] | [X] | Kamel |
| low(BDD_ID f) | [X] | [X] | Kamel |
| high(BDD_ID f) | [X] | [X] | Kamel |
| nodeData(BDD_ID f) | [X] | [X] | Victor |
| ite(BDD_ID i, BDD_ID t, BDD_ID e) | [X] | [X] | Victor |
| coFactorTrue(BDD_ID f, BDD_ID x) | [X] | [X] | Kamel |
| coFactorFalse(BDD_ID f, BDD_ID x) | [X] | [X] | Kamel |
| coFactorTrue(BDD_ID f) | [X] | [X] | Kamel |
| coFactorFalse(BDD_ID f) | [X] | [X] | Kamel |
| and2(BDD_ID a, BDD_ID b) | [X] | [X] | Victor |
| or2(BDD_ID a, BDD_ID b) | [X] | [X] | Victor |
| xor2(BDD_ID a, BDD_ID b) | [X] | [X] | Victor |
| neg(BDD_ID a) | [X] | [X] | Victor |
| nand2(BDD_ID a, BDD_ID b) | [X] | [X] | Victor |
| nor2(BDD_ID a, BDD_ID b) | [X] | [X] | Victor |
| xnor2(BDD_ID a, BDD_ID b) | [X] | [X] | Victor |
| getTopVarName(const BDD_ID &root) | [X] | [X] | Kamel |
| findNodes(const BDD_ID &root, std::set<BDD_ID> &nodes_of_root) | [X] | [X] | Kamel |
| findVars(const BDD_ID &root, std::set<BDD_ID> &vars_of_root) | [X] | [X] | Kamel |
| uniqueTableSize() | [X] | [X] | Victor |
| visualizeBDD(std::string filepath, BDD_ID &root) | [X] | [-] | Victor |
- [] TODO
- DONE
| Function Name | Implemented | Person |
|---|---|---|
| Hash Table for Unique Table | [X] | Victor |
| Caching for Computed Table | [] | Kamel |
| Merge Node and Node Data | [X] | Victor |
| Create scripts for automated verification | [X] | Kamel |
| Complemented Edges | [] | Kamel |
| Standard Triples | [X] | Victor |
| Label Garbage Collection | [X] | Victor |
- TODO
- [] DONE
| Function Name | Implemented | Tested | Person |
|---|---|---|---|
| ReachabilityInterface() | [X] | [X] | Victor |
| ~ReachabilityInterface() | [-] | [-] | Victor |
| getStates() | [X] | [-] | Victor |
| getInputs() | [X] | [-] | Victor |
| isReachable() | [-] | [] | Kamel |
| stateDistance() | [X] | [X] | Victor |
| setTransitionFunctions() | [X] | [X] | Victor |
| setInitState() | [X] | [X] | Victor |
| getTransitionFunctions() | [X] | [-] | Kamel |
| getInitState() | [X] | [-] | Kamel |
Lucas Deutschmann & Philipp Schmitz - eit-vds-cp@rptu.de
Thank you Veli Durmuşcan, Shreya Vithal Kulhalli and Osama Omar Youssif Ayoub for the work on this README.md.
You might find helpful links below.