diff --git a/include/util/cover_to_bdd.hpp b/include/util/cover_to_bdd.hpp index c9be00d..3405cef 100644 --- a/include/util/cover_to_bdd.hpp +++ b/include/util/cover_to_bdd.hpp @@ -1,133 +1,194 @@ // Copyright 2025 Oliver Theimer #pragma once +#include + #include "../bbdd/include/bbdd_node.hpp" #include "bdd.h" +#include "partition.hpp" #include "util.hpp" #define LEFT_CHILD(node) node.children[0].index #define RIGHT_CHILD(node) node.children[1].index #define CUBE(node) ntk._storage->data.covers[node.data[1].h1] using namespace mockturtle; +/// node -> bdd root; refcounting keeps the roots alive across autoreorder +using bdd_memo_t = std::unordered_map; + /** * @brief recursively creates a bdd based on the given network * + * Recursion stops at leaf_map leaves (PIs, plus boundary nets when + * partitioned). + * * @tparam Ntk which network type is used as an input to the function * @param ntk input network which should be converted to bdd + * @param leaf_map maps the leaves of the block to their bdd variable ids * @param node_i current network node which is currently converted is used for * the recursion + * @param memo maps an already converted network node to its bdd root * @return return root bdd node of the created binary decision diagram */ -template static bdd create_bdd(Ntk &ntk, const auto &node_i) { +template +static bdd create_bdd(Ntk &ntk, leaf_map_t const &leaf_map, const auto &node_i, + bdd_memo_t &memo) { static_assert(has_is_ci_v, "Ntk does not implement the is_ci method"); const auto &node = ntk._storage->nodes[node_i]; bdd f, g, result; - bbdd_op_t op = Util::cube_to_bbdd_op(CUBE(node)); - if (node.children.size() != 2 && node.children.size() != 1) { - if (node_i == 1) { + + if (node_i == 1) { #ifdef DEBUG_BDD - printf("[INFO] cover to bdd: constant 1 node\n"); + printf("[INFO] cover to bdd: constant 1 node\n"); #endif - return bdd_true(); - } - if (node_i == 0) { + return bdd_true(); + } + if (node_i == 0) { #ifdef DEBUG_BDD - printf("[INFO] cover to bdd: constant 0 node\n"); + printf("[INFO] cover to bdd: constant 0 node\n"); #endif - return bdd_false(); - } - assert(ntk.is_ci(node_i)); + return bdd_false(); + } + + // block leaf (PI or boundary net) -> variable. Must precede the fanin + // dispatch: boundary nets have children. + if (leaf_map[node_i]) { assert(node_i < pow(2, 31)); - assert(node_i - 2 < ntk._storage->inputs.size()); + assert(leaf_map[node_i] - 2 < leaf_map.size()); #ifdef DEBUG_BDD - printf("[INFO] cover to bdd: base case input: %d\n", node_i); + printf("[INFO] cover to bdd: base case leaf: %d\n", node_i); #endif - return bdd_ithvar(node_i - 2); + return bdd_ithvar(leaf_map[node_i] - 2); } + + // memoised: reconvergent fanout is otherwise exponential + auto cached = memo.find(node_i); + if (cached != memo.end()) { + return cached->second; + } + assert(node.children.size() == 2 || node.children.size() == 1); + bbdd_op_t op = Util::cube_to_bbdd_op(CUBE(node)); + // all the logic gates except buf and inv if (node.children.size() == 2) { - node_index_t f_i = LEFT_CHILD(node), g_i = RIGHT_CHILD(node); - f = create_bdd(ntk, LEFT_CHILD(node)); + f = create_bdd(ntk, leaf_map, LEFT_CHILD(node), memo); #ifdef DEBUG_BDD printf("[INFO] cover to bdd: return from f\n"); #endif - g = create_bdd(ntk, RIGHT_CHILD(node)); + g = create_bdd(ntk, leaf_map, RIGHT_CHILD(node), memo); #ifdef DEBUG_BDD printf("[INFO] cover to bdd: merge %d %s %d\n", f, bbdd_op_s[op].c_str(), g); #endif switch (op) { case bbdd_and: result = bdd_apply(f, g, bddop_and); break; case bbdd_xor: result = bdd_apply(f, g, bddop_xor); break; case bbdd_xnor: result = bdd_not(bdd_apply(f, g, bddop_xor)); break; case bbdd_or: result = bdd_apply(f, g, bddop_or); break; case bbdd_nand: result = bdd_apply(f, g, bddop_nand); break; case bbdd_nor: result = bdd_apply(f, g, bddop_nor); break; default: printf("%s\n", bbdd_op_s[op].c_str()); assert(false && "not implemented yet"); break; } + memo.emplace(node_i, result); return result; } else { // buf and inverter nodes - f = create_bdd(ntk, LEFT_CHILD(node)); - // TODO how to invert + f = create_bdd(ntk, leaf_map, LEFT_CHILD(node), memo); if (op == bbdd_inv) { #ifdef DEBUG_BDD printf("[INFO] cover to bdd: negate\n"); #endif result = bdd_not(f); + memo.emplace(node_i, result); return result; } #ifdef DEBUG_BDD printf("[INFO] cover to bdd: buffer\n"); #endif + memo.emplace(node_i, f); return f; } } +/** + * @brief converts one block of a partition into a bdd forest + * + * One bdd per root, appended to output_map. The caller reinitialises BuDDy per + * block with at least one variable per leaf. + * + * @tparam Ntk template of network type that should be used + * @param ntk network that holds the block + * @param block block that should be converted + * @param leaf_map maps the leaves of the block to their bdd variable ids + * @param root_names name of each root of the block, in the same order + * @param output_map collects the root of every diagram with its name + */ +template +void block_to_bdd(Ntk &ntk, block_t const &block, leaf_map_t const &leaf_map, + std::vector const &root_names, + std::vector> &output_map) { + assert(block.roots.size() == root_names.size()); + // shared so common cones are built once + bdd_memo_t memo; + for (size_t i = 0; i < block.roots.size(); i++) { + output_map.emplace_back(create_bdd(ntk, leaf_map, block.roots[i], memo), + root_names[i]); + } +} + /** * @brief main interface function that handles the conversion to a bdd from a given input network type * * @tparam Ntk network type that is used as an input to the conversion * @param ntk network that should be converted to a bdd * @param output_map outputmap that stores the pointers to the root nodes of each output in the network */ template void cover_to_bdd(Ntk &ntk, std::vector> &output_map) { static_assert(has_foreach_co_v, "Ntk does not implement the foreach_pi method"); static_assert(has_get_node_v, "Ntk does not implement the get_node method"); static_assert(has_set_visited_v, "Ntk does not implement the set_visited method"); static_assert(has_visited_v, "Ntk does not implement the set_visited method"); int index = ntk._storage->inputs.size() + 2; - ntk.foreach_co([ntk, &index, &output_map](const auto &node_i) { + + leaf_map_t leaf_map = make_leaf_map( + ntk._storage->nodes.size(), + std::vector(std::begin(ntk._storage->inputs), + std::end(ntk._storage->inputs))); + + // shared so common cones are built once + bdd_memo_t memo; + ntk.foreach_co([&ntk, &index, &output_map, &memo, + &leaf_map](const auto &node_i) { const auto &node = ntk.get_node(node_i); - auto &n = ntk._storage->nodes[node_i]; - bdd output = create_bdd(ntk, node); + bdd output = create_bdd(ntk, leaf_map, node, memo); output_map.emplace_back(output, ntk.get_signal_name(index)); +#ifdef DEBUG_BDD bdd_printtable(output); +#endif index++; }); } diff --git a/src/convert_bdd.cpp b/src/convert_bdd.cpp index 7af27e2..efe542d 100644 --- a/src/convert_bdd.cpp +++ b/src/convert_bdd.cpp @@ -1,149 +1,464 @@ // Copyright 2025 Oliver Theimer #include #include #include +#include #include #include +#include +#include #include #include #include #include #include #include #include "bdd.h" #include "mockturtle/io/write_blif.hpp" #include "mockturtle/networks/cover.hpp" #include "util/cover_to_bdd.hpp" +#include "util/partition.hpp" -int write_blif_recursive(std::ofstream &blif_file, cover_network cover, - const BDD &node, int next_index, bool output) { +/** + * @brief initial size of the BuDDy node table for one block + * + * As block_table_size in convert_bbdd, but only an initial size: BuDDy grows + * on demand. + * + * @param leaf_count number of variables of the block + * @param table_size upper bound requested on the command line + * @return initial node table size for this block + */ +static int block_node_table(size_t leaf_count, int table_size) { + const uint32_t shift = static_cast(std::min(leaf_count, 17)); + uint64_t wanted = 8ull * (1ull << shift); + if (wanted < 16384ull) { + wanted = 16384ull; + } + if (wanted > static_cast(table_size)) { + wanted = static_cast(table_size); + } + return static_cast(wanted); +} + +/** + * @brief writes the diagram below one node as blif + * + * @param blif_file netlist that is being written + * @param signal_map name of every variable of the block, indexed by variable + * @param prefix namespace for the node ids of this block, empty for a single + * block so that an unpartitioned run keeps writing the netlist it always did + * @param node diagram node to write + * @param emitted nodes already defined in this block + * @param output whether this is a root, whose line carries the output name + */ +int write_blif_recursive(std::ofstream &blif_file, + std::vector const &signal_map, + std::string const &prefix, const BDD &node, + std::unordered_set &emitted, bool output) { if (node < 2) { return node; } - int low_out = - write_blif_recursive(blif_file, cover, bdd_low(node), next_index, false); - int high_out = write_blif_recursive(blif_file, cover, bdd_high(node), - next_index++, false); - blif_file << ".names " << cover.signal_map[bdd_var(node)] << " "; + // define each node once; roots still get their own line, which carries the + // output name + if (!output && !emitted.insert(node).second) { + return node; + } + int low_out = write_blif_recursive(blif_file, signal_map, prefix, + bdd_low(node), emitted, false); + int high_out = write_blif_recursive(blif_file, signal_map, prefix, + bdd_high(node), emitted, false); + blif_file << ".names " << signal_map[bdd_var(node)] << " "; if (IS_TERM(low_out)) { if (low_out == 0) { blif_file << "$false "; } else { blif_file << "$true "; } } else { - blif_file << std::to_string(low_out); + blif_file << prefix << std::to_string(low_out); } blif_file << " "; if (IS_TERM(high_out)) { if (high_out == 0) { blif_file << "$false "; } else { blif_file << "$true "; } } else { - blif_file << std::to_string(high_out) << " "; - } - /*blif_file << std::format( - ".names {} {} {} {}", cover.signal_map[bdd_var(node)], - IS_TERM(low_out) ? (low_out == 0 ? "$false" : "$true") - : std::to_string(low_out), - IS_TERM(high_out) ? (high_out == 0 ? "$false" : "$true") - : std::to_string(high_out), - !output ? std::to_string(node) : "");*/ + blif_file << prefix << std::to_string(high_out) << " "; + } if (!output) { - blif_file << std::to_string(node); + blif_file << prefix << std::to_string(node); blif_file << "\n0-1 1\n11- 1\n"; } return node; } -void write_blif(std::string filename, mockturtle::cover_network cover, - std::vector> output_map) { - std::ofstream blif_file(filename); - blif_file << ".model " + cover.get_module_name() + "\n"; - blif_file << ".inputs"; - for (unsigned int i = 0; i < cover.signal_map.size(); i++) { - blif_file << " " << cover.signal_map[i]; - if (i + 1 == cover._storage->inputs.size()) { - blif_file << "\n.outputs"; - } - } - blif_file << "\n.names $true\n1\n"; - blif_file << ".names $false\n"; - int next_index = cover._storage->inputs.size() + 1; - for (std::pair out_map : output_map) { +/** + * @brief writes every diagram of one block into the open netlist + * + * @param blif_file netlist that is being written + * @param signal_map name of every variable of the block, indexed by variable + * @param prefix namespace for the node ids of this block + * @param output_map root of every diagram of the block with its name + */ +void write_block_body(std::ofstream &blif_file, + std::vector const &signal_map, + std::string const &prefix, + const std::vector> &output_map) { + std::unordered_set emitted; + for (const std::pair &out_map : output_map) { if (out_map.first == bdd_true()) { blif_file << ".names " << out_map.second << "\n1\n"; } else if (out_map.first == bdd_false()) { blif_file << ".names " << out_map.second << "\n0\n"; } else { - write_blif_recursive(blif_file, cover, out_map.first.id(), next_index, - true); + write_blif_recursive(blif_file, signal_map, prefix, out_map.first.id(), + emitted, true); blif_file << out_map.second << "\n0-1 1\n11- 1\n"; } } - blif_file << ".end\n"; } -int get_bdd_height(BDD node) { +// memoised: one visit per node, not per path +int get_bdd_height(BDD node, std::unordered_map &heights) { if (node < 2) { return 0; } - int low_height = get_bdd_height(bdd_low(node)); - int high_height = get_bdd_height(bdd_high(node)); - return std::max(low_height, high_height) + 1; + auto cached = heights.find(node); + if (cached != heights.end()) { + return cached->second; + } + int low_height = get_bdd_height(bdd_low(node), heights); + int high_height = get_bdd_height(bdd_high(node), heights); + int height = std::max(low_height, high_height) + 1; + heights.emplace(node, height); + return height; } -int get_total_height(std::vector> output_map) { +int get_total_height(const std::vector> &output_map) { int max_height = -1; - for (std::pair out_map : output_map) { - int current_height = get_bdd_height(out_map.first.id()); + std::unordered_map heights; + for (const std::pair &out_map : output_map) { + int current_height = get_bdd_height(out_map.first.id(), heights); if (current_height > max_height) { max_height = current_height; } } return max_height; } +/// shared node count of a block's diagrams, so that nodes several roots have in +/// common are counted once +static uint64_t block_node_count( + const std::vector> &output_map) { + // bdd.h maps bdd_anodecount to the C++ overload taking bdd, not raw ids + std::vector roots; + roots.reserve(output_map.size()); + for (const std::pair &out_map : output_map) { + roots.push_back(out_map.first); + } + if (roots.empty()) { + return 0; + } + return static_cast( + bdd_anodecount(roots.data(), static_cast(roots.size()))); +} + int main(int argc, char *argv[]) { + // -o: where the netlist and stats go + std::string out_dir = "temp"; + // maximum input support per block, 0 disables partitioning + uint32_t max_inputs = 0; + // -g: support cap for gain-driven merging, 0 = off + uint32_t gain_cap = 0; + int table_size = 300000; + int cache_size = 10000; + int opt; + while ((opt = getopt(argc, argv, "o:n:g:t:c:")) != -1) { + switch (opt) { + case 'o': + out_dir = optarg; + break; + case 'n': { + char *endptr = nullptr; + long parsed = std::strtol(optarg, &endptr, 10); + if (*endptr != '\0' || parsed < 0) { + std::cerr << "[ERROR] Invalid integer for option -n: " << optarg + << std::endl; + return EXIT_FAILURE; + } + if (parsed != 0 && parsed < 2) { + std::cerr << "[ERROR] -n must be 0 (disabled) or at least 2\n"; + return EXIT_FAILURE; + } + max_inputs = static_cast(parsed); + break; + } + case 'g': { + char *endptr = nullptr; + long parsed = std::strtol(optarg, &endptr, 10); + if (*endptr != '\0' || parsed < 0) { + std::cerr << "[ERROR] Invalid integer for option -g: " << optarg + << std::endl; + return EXIT_FAILURE; + } + gain_cap = static_cast(parsed); + break; + } + case 't': { + char *endptr = nullptr; + table_size = std::strtol(optarg, &endptr, 10); + if (*endptr != '\0' || table_size <= 0) { + std::cerr << "[ERROR] Invalid integer for option -t: " << optarg + << std::endl; + return EXIT_FAILURE; + } + break; + } + case 'c': { + char *endptr = nullptr; + cache_size = std::strtol(optarg, &endptr, 10); + if (*endptr != '\0' || cache_size <= 0) { + std::cerr << "[ERROR] Invalid integer for option -c: " << optarg + << std::endl; + return EXIT_FAILURE; + } + break; + } + default: + std::cerr << "Usage: " << argv[0] + << " [-n max_inputs] [-g gain_cap] [-t table_size] " + "[-c cache_size] [-o output_dir] " + << std::endl; + return EXIT_FAILURE; + } + } + if (optind >= argc) { std::cout << "[ERROR] input file in blif format is missing\n"; - std::cerr << "[INFO] Usage: " << argv[0] << " " << std::endl; + std::cerr << "[INFO] Usage: " << argv[0] + << " [-n max_inputs] [-o output_dir] " << std::endl; return EXIT_FAILURE; } std::string benchmark(argv[optind]); if (!std::filesystem::exists(benchmark)) { std::cout << "[ERROR] File does not exist\n"; return EXIT_FAILURE; } std::filesystem::path path(benchmark); std::string base_name = path.stem().string(); mockturtle::cover_network cover; - // lorina::diagnostic_engine diag; if (lorina::read_blif(benchmark, mockturtle::blif_reader(cover)) != lorina::return_code::success) { std::cout << "[ERROR] While Lorina tried to read in file\n"; return EXIT_FAILURE; } - std::vector> output_map; + printf("[INFO] cover with %zu nodes\n", cover._storage->nodes.size()); + + ////////////////////////////////////////////////////////////////////////// + // partition the network into blocks with a bounded input support + ////////////////////////////////////////////////////////////////////////// + std::vector blocks = partition_cover(cover, max_inputs); + assert(partition_is_valid(cover, blocks, max_inputs)); + + ////////////////////////////////////////////////////////////////////////// + // merge further, but only where the merged diagram is measurably smaller + ////////////////////////////////////////////////////////////////////////// + if (gain_cap > max_inputs && max_inputs != 0 && blocks.size() > 1) { + size_t const before = blocks.size(); + // trial build, same as the writer + auto block_cost = [&](block_t const &b) -> uint64_t { + leaf_map_t leaf_map = + make_leaf_map(cover._storage->nodes.size(), b.leaves); + std::vector root_names(b.roots.size(), "t"); + const size_t vars = std::max(b.leaves.size(), 1); + + bdd_init(block_node_table(b.leaves.size(), table_size), cache_size); + bdd_setvarnum(static_cast(vars)); + uint64_t nodes = 0; + { + std::vector> outs; + block_to_bdd(cover, b, leaf_map, root_names, outs); + nodes = block_node_count(outs); + // the roots have to be released before the instance they live in + } + bdd_done(); + return nodes; + }; + + merge_blocks_by_gain(cover, blocks, gain_cap, /*max_passes=*/3u, + /*max_candidates=*/8u, block_cost); + assert(partition_is_valid(cover, blocks, gain_cap)); + printf("[INFO] gain merge (cap %u): %zu block(s) -> %zu\n", gain_cap, + before, blocks.size()); + } + + size_t max_support = 0, total_support = 0, max_gates = 0; + for (block_t const &b : blocks) { + max_support = std::max(max_support, b.leaves.size()); + total_support += b.leaves.size(); + max_gates = std::max(max_gates, b.gates.size()); + } + printf("[INFO] %zu block(s), support max %zu avg %.1f, largest block %zu " + "gates\n", + blocks.size(), max_support, + blocks.empty() ? 0.0 + : static_cast(total_support) / blocks.size(), + max_gates); + + ////////////////////////////////////////////////////////////////////////// + // give every signal that appears in the output netlist a name + ////////////////////////////////////////////////////////////////////////// + std::vector canonical(cover._storage->nodes.size()); + canonical[0] = "$false"; + canonical[1] = "$true"; + for (uint64_t const &pi : cover._storage->inputs) { + canonical[pi] = cover.get_signal_name(pi); + } + + // primary outputs in declaration order, together with their driver + std::vector> po_list; + { + uint32_t index = cover._storage->inputs.size() + 2; + cover.foreach_co([&](auto const &f) { + po_list.emplace_back(cover.get_node(f), cover.get_signal_name(index)); + index++; + }); + } + // a root that drives a primary output is named after it, so that the common + // case needs no extra buffer + std::vector po_first(cover._storage->nodes.size()); + for (auto const &po : po_list) { + if (po_first[po.first].empty()) { + po_first[po.first] = po.second; + } + } + + // every root has to be named before any block is written, because a block + // may use a root of a later block as one of its leaves + for (block_t const &b : blocks) { + for (uint64_t const &r : b.roots) { + if (canonical[r].empty()) { + canonical[r] = + !po_first[r].empty() ? po_first[r] : "part_w" + std::to_string(r); + } + } + } + + ////////////////////////////////////////////////////////////////////////// + // write the netlist: one header, then the diagrams of every block + ////////////////////////////////////////////////////////////////////////// + std::string out_file = out_dir + "/" + base_name + "_bdd.blif"; + std::ofstream blif(out_file); + if (!blif) { + std::cerr << "[ERROR] cannot open " << out_file << " for writing\n"; + return EXIT_FAILURE; + } + blif << ".model " << cover.get_module_name() << "\n"; + blif << ".inputs"; + for (uint64_t const &pi : cover._storage->inputs) { + blif << " " << canonical[pi]; + } + blif << "\n.outputs"; + for (auto const &po : po_list) { + blif << " " << po.second; + } + blif << "\n.names $true\n1\n"; + blif << ".names $false\n"; + + uint64_t total_nodes = 0; + int max_height = 0; + int peak_table = 0; + for (size_t id = 0; id < blocks.size(); id++) { + block_t const &b = blocks[id]; + + leaf_map_t leaf_map = + make_leaf_map(cover._storage->nodes.size(), b.leaves); + + // names of the block's variables, indexed by BuDDy variable number, which + // is the leaf map's id minus 2 + std::vector signal_map; + signal_map.reserve(b.leaves.size()); + for (uint64_t const &l : b.leaves) { + signal_map.push_back(canonical[l]); + } + std::vector root_names; + root_names.reserve(b.roots.size()); + for (uint64_t const &r : b.roots) { + root_names.push_back(canonical[r]); + } + + // a fresh instance per block: a BuDDy variable number means a different + // signal in every block, so blocks must not share a variable ordering + const size_t vars = std::max(b.leaves.size(), 1); + bdd_init(block_node_table(b.leaves.size(), table_size), cache_size); + bdd_setvarnum(static_cast(vars)); + bdd_autoreorder(BDD_REORDER_SIFT); + if (blocks.size() == 1) { + printf("[INFO] init with %zu variables\n", b.leaves.size()); + } + + { + std::vector> output_map; + block_to_bdd(cover, b, leaf_map, root_names, output_map); + // bdd_reorder_siftite is the same but repeats until no more progress is + // done + bdd_reorder(BDD_REORDER_SIFT); + + const int height = get_total_height(output_map); + if (blocks.size() == 1) { + printf("height after: %d\n", height); + } + max_height = std::max(max_height, height); + total_nodes += block_node_count(output_map); + peak_table = std::max(peak_table, bdd_getnodenum()); + + // a single block owns the whole module, so its node indices are already + // unique and the netlist stays identical to an unpartitioned run + write_block_body(blif, signal_map, + blocks.size() == 1 ? "" : "b" + std::to_string(id) + "_", + output_map); + // the roots have to be released before the instance they live in + } + bdd_done(); + } + + // outputs that are not named after their driver need an explicit buffer: + // a primary input or constant wired straight through, or a second primary + // output on the same driver + for (auto const &po : po_list) { + if (canonical[po.first] != po.second) { + blif << ".names " << canonical[po.first] << " " << po.second << "\n1 1\n"; + } + } + blif << ".end\n"; + blif.close(); + + printf("[INFO] BDD created: %lu nodes, max height %d, peak table use %d\n", + total_nodes, max_height, peak_table); + std::cout << "[INFO] Wrote bdd into " << out_file << "\n"; + + // machine readable summary for the regression runner + std::ofstream stats(out_dir + "/" + base_name + "_bdd_stats.csv"); + if (stats) { + stats << "blocks;max_support;avg_support;max_block_gates;bdd_nodes;" + "max_height;peak_table;seed_n;gain_cap\n"; + stats << blocks.size() << ";" << max_support << ";" + << (blocks.empty() + ? 0.0 + : static_cast(total_support) / blocks.size()) + << ";" << max_gates << ";" << total_nodes << ";" << max_height << ";" + << peak_table << ";" << max_inputs << ";" << gain_cap << "\n"; + } - bdd_init(300000, 10000); - bdd_setvarnum(cover._storage->inputs.size()); - bdd_autoreorder(BDD_REORDER_SIFT); - printf("[INFO] init with %zu variables\n", cover._storage->inputs.size()); - cover_to_bdd(cover, output_map); - // bdd_reorder_siftite is the same but repeats until no more progress is done - bdd_reorder(BDD_REORDER_SIFT); - printf("height after: %d\n", get_total_height(output_map)); - write_blif("temp/" + base_name + "_bdd.blif", cover, output_map); - bdd_done(); return EXIT_SUCCESS; }