CAL

     

CAL is a BDD package [Bryant86] that uses breadth-first algorithms [Ochi93, Ashar94, Sanghavi96] to exploit a locality of BDD nodes on disk. This allows one to obtain a high performance when manipulating Binary Decision Diagrams, even when they outgrow the memory limit of the given machine.

This project was developed in the late 90's at EECS at UC Berkeley. In 2022, the Logic and Semantics group at Aarhus University have brought this project back from the grave by upgrading it to be built with CMake and by adding a clean C++ API.

Table of Contents

• Documentation
• Usage
• License
• References

Documentation

An overview of all functions can be found as simple text file in calDoc.txt or as an easier to navigate HTML page in the docs/ folder which is hosted on GitHub Pages.

Usage

To get started with CAL, you need to place the repository somewhere on your machine. The simplest way to do so is to add it as a submodule inside the Git repository of your project.

git submodule add https://github.com/SSoelvsten/cal external/cal
git submodule update

Then include the following line in your project's CMakeLists.txt.

add_subdirectory (external/cal cal)

Finally, every single executable target is linked to CAL in the CMakeLists.txt file with the following lines.

add_executable(<target> <source>)
target_link_libraries(<target> cal)

At this point, you may include the C header <cal.h> or the C++ header <calObj.hh> and get started on programming.

License

This software is provided as-is and with permission to copy, modify, and distribute. See LICENSE for more details.

References

• [Ashar94] Pranav Ashar and Matthew Cheong. “Efficient breadth-first manipulation of binary decision diagrams”. In: Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design. (1994)

• [Bryant86] Randal E. Bryant. “Graph-Based Algorithms for Boolean Function Manipulation”. In: IEEE Transactions on Computers. (1986)

• [Ochi93] Hiroyuki Ochi, Koichi Yasuoka, and Shuzo Yajima. “Breadth-first manipulation of very large binary-decision diagrams”. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD), (1993)

• [Sanghavi96 Jagesh V. Sanghavi, Rajeev K. Ranjan, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli. “High performance BDD package by exploiting memory hierarchy”. In: Proceedings of the 33rd Annual Design Automation Conference (1996)

• [Ranjan97] Rajeev K. Ranjan, Wilsin Gosti, Robert K. Brayton, and Alberto Sangiovanni-Vincenteili. “Dynamic reordering in a breadth-first manipulation based BDD package: challenges and solutions”. In: Proceedings International Conference on Computer Design VLSI in Computers and Processors (1997)