Freddy

FrEDDY is a Framework to Engineer Decision Diagrams Yourself for efficient solving of problems in VLSI CAD.

:dart: Features

• Level-based unique tables for DD optimization
• Automatic memory management to delete dead DDs (delayed)
• Dynamic cache to speed up DD operations
• Optimized operations for DD manipulation
• Manager concept enabling instances to coexist
• Development of custom DD types based on the manager
• Registration of custom operations with the cache
• Overloaded wrapping of DD handlers to increase usability
• Parameter configuration for specific problem solving
• Detailed output for effective debugging
• And much more

:rocket: Getting Started

The installation of FrEDDY is described first. Second, it's explained how a DD type can be used to solve a problem.

:wrench: Installation

FrEDDY is designed as a header-only library that can be easily integrated into external projects. To integrate FrEDDY into your CMake project, simply clone it inside your project directory or add it as a Git submodule, and include the following lines of code in its CMakeLists.txt:

add_subdirectory(freddy)
target_link_libraries(<target> freddy)

:information_source: Depending on where FrEDDY is located, you may need to adjust the path accordingly.

Note that this stage may take some time depending on your system configuration. For example, FrEDDY relies on certain Boost libraries like Unordered, which offers high-performance hash containers. If this dependency cannot be found locally, it'll be downloaded from an external repository at configure time, with the required Boost modules automatically added to your build system.

:computer: Usage

To solve problems such as equivalence checking of multipliers, include the header of an appropriate reduced and ordered DD type, such as a multiplicative binary moment diagram, and initialize the corresponding manager in your code:

#include <freddy/dd/bmd.hpp>

int main()
{
    freddy::bmd_manager mgr;
}

A correspondence is generally proven by interpreting the binary signals $x_1, \dots, x_n$ of a logical network $f$ using an encoding function $e$ and comparing the result to a word-level specification $g$: $e(f(x_1, \dots, x_n)) = g(e(x_1), \dots, e(x_n))$.

In this example, a bit-level implementation f of a 2-bit multiplier is generated using symbolic simulation:

/* includes */

int main()
{
    /* initialization */

    auto const a1 = mgr.var("a1");
    auto const b1 = mgr.var("b1");
    auto const a0 = mgr.var("a0");
    auto const b0 = mgr.var("b0");
    std::array<freddy::bmd, 8> s;
    s[0] = a0 & b0;
    s[1] = a0 & b1;
    s[2] = a1 & b0;
    s[3] = a1 & b1;
    s[4] = s[1] ^ s[2];
    s[5] = s[1] & s[2];
    s[6] = s[3] ^ s[5];
    s[7] = s[3] & s[5];
    std::vector<freddy::bmd> const f{s[0], s[4], s[6], s[7]};
}

While the bmd_manager handles BMD operations, the overloaded wrapper bmd allows direct access to a BMD. In this context, the word-level specification g can be realized as a sum of weighted bits:

/* includes */

int main()
{
    /* initialization */
    
    /* bit-level implementation */

    auto const g = mgr.unsigned_bin({a0, a1}) * mgr.unsigned_bin({b0, b1});
}

The multiplier can now be formally verified by interpreting the network outputs as a word:

/* includes */

int main()
{
    /* initialization */
    
    /* bit-level implementation */
    
    /* word-level specification */

    return !(mgr.unsigned_bin(f) == g);
}

:warning: Even though throwing exceptions – for example, when multiplying very large BMD constants – is unlikely, they should still be handled using catch blocks.

Whereas encodings such as unsigned_bin (unsigned binary) are specific to BMDs, each DD type supports methods that are common across all types. One such method called dump_dot involves drawing edges and nodes with DOT. The resulting graph can be rendered using a layout engine and looks like the following BMD:

Again, it's possible to adjust various configuration parameters depending on the problem. For instance, the minimum capacity cache_size_hint of the cache can be passed to the manager, which is employed for many other operations beyond multiplication. Here is an overview of the currently configurable parameters:

| Parameter | Default setting | Description | | ------------------ | --------------- | ------------------------------------------------------------------ | | utable_size_hint | 1,679 | Minimum capacity of a unique table | | cache_size_hint | 215,039 | Minimum capacity of the operation cache | | init_var_cap | 16 | Initial capacity of the variable list | | max_node_growth | 1.2 | Permitted node growth factor during reordering | | heap_mem_limit | Unset | Heap usage in bytes before garbage collection (estimated if unset) |

You can also choose how a variable should be decomposed, provided the DD type supports it. Although the positive Davio expansion (pD) applies to BMDs, other expansion types, such as the Shannon expansion, are available in the decomposition type list.

To simplify working with multiple DD types at once, it's recommended to include the provided umbrella header.

:white_check_mark: Tests

Tests are split into basic functionality checks and (further) example cases. They can be built with CMake by passing the flag -DFREDDY_TEST=ON on the command line and run using ctest:

$ cmake -B build/Release -DCMAKE_BUILD_TYPE=Release -DFREDDY_TEST=ON
$ cmake --build build/Release --config Release
$ cd build/Release
$ ctest -C Release

For debugging purposes, type Debug instead of Release.

:warning: Compiling in debug mode may negatively impact the performance of FrEDDY.

Additionally, you can add -j k to build on k cores or -v to show in detail the commands used to build.

:handshake: Contributing

Do you want to contribute to FrEDDY? In particular, contributions towards the development of additional DD types are welcome. Since the base manager is abstract, the following pure virtual methods must be implemented within the freddy namespace in the dd directory for basic operations to work:

| Method | Description | | ---------------- |----------------------------------------------------| | agg | Aggregation of an edge weight and a node value | | comb | Adjustment of a weight pair | | complement | Computation of NOT | | conj | Connection of two conjuncts (AND) | | denorm_high | Representation of the high cofactor | | denorm_low | Representation of the low cofactor | | disj | Connection of two disjuncts (OR) | | expanded | Cofactor of a function on a variable not contained | | merge | Evaluation of aggregates (subtrees) | | mul | Multiplicative combination of DDs | | norm_high | Normalization of a node's high child | | norm_is_needed | Graph normalization check | | norm_low | Normalization of a node's low child | | norm_weight | Scheme for providing a canonical form | | plus | Additive combination of DDs | | reduced | Application of the DD-dependent reduction rule | | reducible | Test for DD reduction excluding isomorphism | | regw | Regular weight of an edge |

While virtual methods such as ite (if-then-else) can be overridden if specialized behavior is needed, both the contradiction and tautology must be defined using a DD edge weight (EWeight template parameter) and node value (NValue template parameter), which are then passed to the base constructor.

:information_source: If EWeight or NValue aren't built-in types, the equality operator == must be overloaded for hashing purposes. Of course, a custom specialization of std::hash must