diff --git a/include/unique_table.hpp b/include/unique_table.hpp index dd358de..6c29664 100644 --- a/include/unique_table.hpp +++ b/include/unique_table.hpp @@ -1,1249 +1,1279 @@ // Copyright 2025 Oliver Theimer #pragma once #include #include #include #include #include #include #include #include #include #include #include #include "./bbdd_node.hpp" #include "./bbdd_types.hpp" #include "./chain_variable_ordering.hpp" #include "./computed_table.hpp" #include "./extend_table.hpp" // idea from CUDD package #define SIZEOF_VOID_P 8 #define SIZEOF_INT 4 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 typedef uint32_t bbdd_halfword_t; #else typedef uint16_t bbdd_halfword_t; #endif #define REF(n) entries[n].ref #define LEVEL(n) entries[n].node.cvo_lvl #define EQ(n) entries[n].node.eq_child #define NEQ(n) entries[n].node.neq_child #define INDEX(n) entries[n].node.index #define NEXT(n) entries[n].next #define NEXT_ENTRY(n) entries[n->next] typedef uint32_t node_index_t; /** * @class variable_relation_t * @brief struct used to store information about a bbdd to generate its truth * table * */ struct variable_relation_t { node_index_t pv; node_index_t sv; bool eq; }; /** * @class table_entry_t * @brief struct that stored a single entry of the hash table * */ struct table_entry_t { bbdd_node_t node; bbdd_halfword_t next; bbdd_halfword_t ref; }; /** * @class output_map_t * @brief struct that maps a bbdd root node to a human readable string * */ struct output_map_t { std::string output; bbdd_node_t *bbdd; }; class Unique_table { enum return_codes { SUCCESS, OUT_OF_MEMORY, TABLE_FULL }; #define NODE(n) entries[n].node #define ENTRY(n) entries[n] private: table_entry_t *entries; node_index_t free_pos; uint32_t capacity; std::string module_name; std::vector free_slots; /** * @brief swap two adhacent variables in variable ordering * * @param pos_b position of the first variable * @param pos_c position of the second variable */ void swap_variable_order(node_index_t pos_b, node_index_t pos_c) { assert(pos_b + 1 == pos_c); node_index_t temp = (*cvo)[pos_b].in; (*cvo)[pos_b].in = (*cvo)[pos_c].in; (*cvo)[pos_c].in = temp; (*cvo)[(*cvo)[pos_b].in % num_inputs].pos = pos_b; (*cvo)[(*cvo)[pos_c].in % num_inputs].pos = pos_c; } /** * @brief recursive helper function to count the number of nodes in bbdd * * @param node bbdd root node whose size should be evaluated * @return number of nodes in subgraph denoted by root node */ uint32_t get_number_nodes_recursive(bbdd_node_t *node) { if (IS_TERM(node->index) || MARKED(node)) { return 0; } SET_MARKED(node); uint32_t neq_size = get_number_nodes_recursive(get_node_p(node->neq_child)); uint32_t eq_size = get_number_nodes_recursive(get_node_p(node->eq_child)); return (neq_size + eq_size) + 1; } /** * @brief recursive helper function to dump a bbdd into a dot file format * * @param file dot file in which the output should be written to * @param node root node whose subgraph should be printed into dot file format * @return node index used for recursive print */ node_index_t recursive_dump_dot(std::ofstream &file, bbdd_node_t *node) { if (IS_TERM(node->index) || MARKED(node)) { return node->index; } if (node->cvo_lvl.sv != INT_MAX) { file << "\n\t" << (GET_INDEX(node)) << " [label=\"" << node->ref << "" << (GET_INDEX(node)) << ": " << node->cvo_lvl.pv << "," << node->cvo_lvl.sv << "\"]\n"; } else { file << "\n\t" << (GET_INDEX(node)) << " [label=\"" << node->ref << "" << (GET_INDEX(node)) << ": " << node->cvo_lvl.pv << "," << 1 << "\"]\n"; } SET_MARKED(node); recursive_dump_dot(file, get_node_p(node->neq_child)); recursive_dump_dot(file, get_node_p(node->eq_child)); file << "\t" << (GET_INDEX(node)) << " -- " << node->neq_child << "[style=\"dashed\"]\n"; //<< "[style=\"dashed\", label=<>]\n"; file << "\t" << (GET_INDEX(node)) << " -- " << node->eq_child << "\n"; return (GET_INDEX(node)); } /** * @brief return the ith bit of an integer * * @param integer integer from which the bit should be retrieved * @param bits number of bits in the integer * @param index position of bit that should be retrieved * @return boolean rather the bit is high (true) or low (false) */ bool get_ith_bit(node_index_t integer, node_index_t bits, uint8_t index) { return integer & (1 << ((bits - 1) - index)); } /** * @brief helper function that is used to collect truth table entries based on * a variable relation list * * @param var_rel vector of variable relation entries retrieved from * traversing the bbdd * @param inputs number of inputs to the truth table * @param tt vector of truth table values that should be filled by this * function * @param value that should be inserted into the truth table */ void insert_tt_value(std::vector var_rel, node_index_t inputs, std::vector &tt, bool value) { if (!value) { return; } for (variable_relation_t rel : var_rel) { #ifdef DEBUG_TABLE printf("%d %s %d\n", rel.pv, rel.eq ? "=" : "!=", rel.sv); #endif } for (uint32_t i = 0; i < tt.size(); i++) { bool insert = true; for (variable_relation_t rel : var_rel) { if (rel.eq) { if (rel.sv == INT_MAX) { if (!get_ith_bit(i, inputs, rel.pv - 2)) { insert = false; } } else if (get_ith_bit(i, inputs, rel.pv - 2) != get_ith_bit(i, inputs, rel.sv - 2)) { insert = false; } } else { if (rel.sv == INT_MAX) { if (get_ith_bit(i, inputs, rel.pv - 2)) { insert = false; } } else if (get_ith_bit(i, inputs, rel.pv - 2) == get_ith_bit(i, inputs, rel.sv - 2)) { insert = false; } } } if (insert && value) { #ifdef DEBUG_TABLE printf("INSERTED %d at : %d %d%d%d%d\n", value, i, get_ith_bit(i, inputs, 3), get_ith_bit(i, inputs, 2), get_ith_bit(i, inputs, 1), get_ith_bit(i, inputs, 0)); #endif tt[i] = value; } } } /** * @brief helper function that is used to recursively fill the truth table of * the target bbdd * * @param node bbdd root node for which the truth table should be created * @param var_rel helper data structure that stores the relation between the * inputs * @param inputs number of inputs to be considered for the truth table * @param tt truth table data structure that should be filled by this function */ void recursive_dump_tt(bbdd_node_t *node, std::vector var_rel, node_index_t inputs, std::vector &tt) { std::vector neq_rel = var_rel; std::vector eq_rel = var_rel; if (IS_TERM(node->index)) { return; } neq_rel.push_back({node->cvo_lvl.pv, node->cvo_lvl.sv, false}); eq_rel.push_back({node->cvo_lvl.pv, node->cvo_lvl.sv, true}); if (node->neq_child == 1) { insert_tt_value(neq_rel, inputs, tt, true); } if (node->eq_child == 1) { insert_tt_value(eq_rel, inputs, tt, true); } recursive_dump_tt(get_node_p(node->neq_child), neq_rel, inputs, tt); recursive_dump_tt(get_node_p(node->eq_child), eq_rel, inputs, tt); } /** * @brief recursive helper function that recursively writes the bbdd into a * blif file format uses only multiplexer and xor nodes * * @param blif_file output filestream in which the bbdd should be written to * @param node root node to the bbdd that should be converted * @param signal_map signal mal between internal indices and human readable * strings * @param output helper variable rather the current node is a output node or * internal node * @return index of the current bbdd node */ uint32_t write_blif_recursive(std::ofstream &blif_file, bbdd_node_t *node, std::vector signal_map, bool output) { if (IS_TERM(node->index) || MARKED(node)) { return GET_INDEX(node); } SET_MARKED(node); uint32_t left_child = write_blif_recursive( blif_file, get_node_p(node->neq_child), signal_map, false); uint32_t right_child = write_blif_recursive( blif_file, get_node_p(node->eq_child), signal_map, false); if (node->cvo_lvl.sv != INT_MAX) { blif_file << ".names " << signal_map[node->cvo_lvl.pv - 2].c_str() << " " << signal_map[node->cvo_lvl.sv - 2].c_str() << " " << std::to_string(GET_INDEX(node)) << "s\n"; } else { blif_file << ".names " << signal_map[node->cvo_lvl.pv - 2].c_str() << " $true " << std::to_string(GET_INDEX(node)) << "s\n"; } blif_file << "00 1\n11 1\n"; blif_file << ".names " << std::to_string(GET_INDEX(node)) << "s "; if (IS_TERM(right_child)) { if (right_child == 0) { blif_file << "$false "; } else { blif_file << "$true "; } } else { blif_file << std::to_string(right_child); } blif_file << " "; if (IS_TERM(left_child)) { if (left_child == 0) { blif_file << "$false "; } else { blif_file << "$true "; } } else { blif_file << std::to_string(left_child); } blif_file << " "; if (!output) { blif_file << std::to_string(GET_INDEX(node)) << "\n"; } if (!output) { blif_file << "0-1 1\n11- 1\n"; } return GET_INDEX(node); } /** * @brief recursive helper function that dumps the bbdd node into a blif file * format and only uses NEMS specific muxxor nodes * * @param blif_file output file in which should the design by written to * @param node root node of the bbdd that should be dumped * @param signal_map map between the internal indices and human readable * string used for the design inputs * @param output boolean that represents if the current bbdd node is an output * or not * @return bbdd node index of the current bbdd node only used during recursion */ uint32_t write_blif_recursive_muxxor(std::ofstream &blif_file, bbdd_node_t *node, std::vector signal_map, bool output) { if (IS_TERM(node->index) || MARKED(node)) { return GET_INDEX(node); } SET_MARKED(node); // format a, b, in0, in1, out // 00-1 1 // 011- 1 // 101- 1 // 11-1 1 uint32_t left_child = write_blif_recursive_muxxor( blif_file, get_node_p(node->neq_child), signal_map, false); uint32_t right_child = write_blif_recursive_muxxor( blif_file, get_node_p(node->eq_child), signal_map, false); // MUXXOR part std::string a, b, in0, in1, out; a = signal_map[node->cvo_lvl.pv - 2].c_str(); if (node->cvo_lvl.sv != INT_MAX) { b = signal_map[node->cvo_lvl.sv - 2].c_str(); } else { b = "$true"; } if (IS_TERM(right_child)) { in1 = right_child == 0 ? "$false" : "$true"; } else { in1 = std::to_string(right_child); } if (IS_TERM(left_child)) { in0 = left_child == 0 ? "$false" : "$true"; } else { in0 = std::to_string(left_child); } blif_file << ".names " << a << " " << b << " " << in0 << " " << in1 << " "; if (!output) { blif_file << std::to_string(GET_INDEX(node)) << "\n"; // blif_file << "0-1 1\n11- 1\n"; blif_file << "00-1 1\n011- 1\n101- 1\n11-1 1\n"; } return GET_INDEX(node); } public: #ifdef CACHE_STATS struct cache_stats_t { uint32_t hits; uint32_t inserts; uint32_t misses; uint32_t chain; uint32_t current_chain; uint32_t extend_hits; uint32_t extend_lookups; uint32_t merge_hits; uint32_t merge_lookups; }; cache_stats_t cache_stats; #endif std::vector output_map; std::vector signal_map; cvo_t *cvo; uint32_t num_inputs; std::unordered_map computed_table; std::unordered_map extend_table; Unique_table() {} /** * @brief return bbdd node based on given index * * @param index for which the bbdd node should be retrieved * @return bbdd node at index */ bbdd_node_t get_node(node_index_t index) { return entries[index].node; } /** * @brief return pointer to node at given index * * @param index for which the pointer to the bbdd node should be retrieved * @return pointer to bbdd node at index */ bbdd_node_t *get_node_p(node_index_t index) { return &entries[index].node; } /** * @brief initialize cvo based on input list, cvo initial ordering strategy * and optional ordering that should be used * * @param inputs list of inputs that should are going to be used in design * @param cvo_opt chain variable ordering initial ordering strategy. Currently * strategies available: cvo_none, cvo_even, cvo_even_reversed, cvo_random, * cvo_input * @param input_cvo list of initial ordering only considered when cvo_opt is * cvo_input */ void init_cvo(std::vector inputs, cvo_init_t cvo_opt, std::vector input_cvo = std::vector()) { cvo = reinterpret_cast(malloc(sizeof(cvo_t))); num_inputs = inputs.size(); init_ordering(inputs, cvo, cvo_opt, input_cvo); } /** * @brief initial signal map with a list of input name strings. Only required * if output should be written to blif file * * @param input_names list of input name strings */ void init_signal_map(std::vector input_names) { for (std::string input : input_names) { this->signal_map.emplace_back(input); } } /** * @brief Clear cache that is used during merge operations */ void clear_computed_table() { computed_table.clear(); } /** * @brief Clear cache that is used during extend operations */ void clear_extend_table() { extend_table.clear(); } /** * @brief Get next free position in the hash table * * @return index of next free position */ uint32_t get_free_pos() { return free_pos; } /** * @brief initialise has table that stores the node information * * @param init_node_count capacity of the hash table * @param module_name name of the module that is represented by the bbdds, * only required for writing the design into blif file format * @return status code depending if the operations was succesful */ int8_t init_table(uint64_t init_node_count, std::string module_name) { if (init_node_count > pow(2, 31)) { std::cerr << "[ERROR] init table: node count is too large\n"; return -1; } this->module_name = module_name; entries = reinterpret_cast( malloc(sizeof(table_entry_t) * init_node_count)); if (entries == NULL) { std::cerr << "[ERROR] init failed, because out of memeory\n"; return OUT_OF_MEMORY; } capacity = init_node_count; for (node_index_t i = 0; i < init_node_count; i++) { // init with zero LEVEL(i).pv = 0; LEVEL(i).sv = 0; EQ(i) = 0; NEQ(i) = 0; NEXT(i) = 0; REF(i) = 0; INDEX(i) = 0; } LEVEL(0).pv = INT_MAX; LEVEL(0).sv = INT_MAX; INDEX(0) = 0; // Constant 1 LEVEL(1).pv = INT_MAX; LEVEL(1).sv = INT_MAX; INDEX(1) = 1; REF(1) = 1; // first empty space after constants free_pos = 2; #ifdef CACHE_STATS cache_stats.hits = 0; cache_stats.inserts = 0; cache_stats.misses = 0; cache_stats.chain = 0; cache_stats.current_chain = 0; cache_stats.extend_lookups = 0; cache_stats.extend_hits = 0; cache_stats.merge_lookups = 0; cache_stats.merge_hits = 0; #endif return SUCCESS; } /** * @brief free hash table */ void free_table() { free(entries); } /** * @brief insert bbdd node into the hash table * * @param node_t bbdd node template that should be inserted * @return pointer to bbdd node in the hash table */ bbdd_node_t *insert_node(bbdd_node_template_t node_t) { #ifdef CACHE_STATS cache_stats.inserts++; #endif assert(node_t.cvo_lvl.sv == INT_MAX || POS(node_t.cvo_lvl.pv, cvo) < POS(node_t.cvo_lvl.sv, cvo)); node_index_t hash = hash_node(node_t, capacity); #ifdef DEBUG_TABLE printf("[INFO] INSERT: trying (%d, %d) %d %d hash: %d\n", node_t.cvo_lvl.pv, node_t.cvo_lvl.sv, node_t.neq_child, node_t.eq_child, hash); #endif if (free_pos >= capacity && free_slots.empty()) { // resize not implemented yet std::cerr << "[ERROR] Unique Table is full resize not implemented yet"; int count = 0; for (int i = 0; i < capacity; i++) { if (entries[i].ref == 0) { count++; } } assert(false); return 0; } table_entry_t *entry = &entries[hash]; node_index_t chain_i = -1; if (entry->ref != 0) { // there is already a node with this hash chain_i = entry->ref; #ifdef CACHE_STATS cache_stats.current_chain = 0; #endif while (true) { // see if that is the node we currently want to insert if (node_eq(entries[chain_i].node, node_t)) { #ifdef DEBUG_TABLE std::cout << "[INFO] INSERT: node hit "; dump_node(&entries[chain_i].node); std::cout << "\n"; #endif #ifdef CACHE_STATS cache_stats.hits++; #endif return &entries[chain_i].node; } // if there is no more node in the chain break and insert at that // position if (NEXT(chain_i) == 0) { #ifdef CACHE_STATS if (cache_stats.current_chain > cache_stats.chain) { cache_stats.chain = cache_stats.current_chain; } #endif break; } chain_i = NEXT(chain_i); #ifdef CACHE_STATS cache_stats.current_chain++; #endif } } node_index_t insert_pos; if (free_slots.empty()) { insert_pos = free_pos; free_pos++; } else { insert_pos = free_slots.back(); free_slots.pop_back(); } // insert node bbdd_node_t node = {0, insert_pos, node_t.cvo_lvl, node_t.neq_child, node_t.eq_child}; get_node_p(node_t.eq_child)->ref++; get_node_p(node_t.neq_child)->ref++; NODE(insert_pos) = node; // extend chain if (chain_i != -1) { #ifdef DEBUG_TABLE std::cout << "[INFO] INSERT: extending chain at " << chain_i << " "; dump_node(&NODE(insert_pos)); std::cout << "\n"; #endif entries[chain_i].next = insert_pos; } else { entry->ref = insert_pos; #ifdef DEBUG_TABLE printf("[INFO] INSERT: no chain "); dump_node(&NODE(insert_pos)); std::cout << "\n"; #endif } #ifdef CACHE_STATS cache_stats.misses++; #endif return &NODE(insert_pos); } /** * @brief delte bbdd node from the hash table * * @param node pointer to bbdd node that should be deleted from the hash table */ void delete_node(bbdd_node_t *node) { node_index_t hash = hash_node(*node, capacity); // assert(entries[hash].ref != 0); node_index_t ref = entries[hash].ref; if (ref == node->index) { // not part of a chain #ifdef DEBUG_TABLE printf("[INFO] DELETE: no chain replacing %d with %d\n", node->index, entries[ref].next); #endif entries[hash].ref = entries[ref].next; free_slots.emplace_back(node->index); } else { // part of a chain get first element table_entry_t *chain_entry = &entries[entries[hash].ref]; for (int i = 0; i < capacity; i++) { if (node_eq(entries[chain_entry->next].node, *node)) { // remove node from chain #ifdef DEBUG_TABLE printf("[INFO] DELETE: chain replacing at %d with %d\n", chain_entry->node.index, entries[node->index].next); #endif chain_entry->next = entries[node->index].next; entries[node->index].next = 0; entries[node->index].node = {0, 0, {0, 0}, 0, 0}; free_slots.emplace_back(node->index); return; } chain_entry = &entries[chain_entry->next]; } dump_table(); std::cout << "[ERROR] Node Node found: " << node->index << "\n"; dump_node(node); std::cout << " with hash " << hash << "\n"; fflush(stdout); assert(false && "node not found"); } } /** * @brief add output map from bbdd node pointer to a string, used for * displaying and blif file purposes * * @param output string to human readable output * @param bbdd root bbdd node that represents output function */ void add_output(std::string output, bbdd_node_t *bbdd) { output_map_t map = {output, bbdd}; bbdd->ref++; output_map.emplace_back(map); } /** * @brief recursively clears marks from bbdd * * @param bbdd root bbdd node for which all marks should be cleared */ void clear_marks(bbdd_node_t *bbdd) { if (IS_TERM(bbdd->index)) { return; } CLEAR_MARKED(bbdd); clear_marks(get_node_p(bbdd->neq_child)); clear_marks(get_node_p(bbdd->eq_child)); } /** * @brief dump hash table entries, only entries with data are printed */ void dump_table() { for (uint64_t i = 0; i < free_pos; i++) { printf("Hash: %6d Ref: %3d Next: %4d Node: ", hash_node(entries[i].node, capacity), entries[i].ref, entries[i].next); dump_node(&entries[i].node); std::cout << "\n"; } for (uint64_t i = free_pos; i < capacity; i++) { if (entries[i].ref != 0) { printf("i: %3lu Ref: %2d Next: %4d Node: \n", i, entries[i].ref, entries[i].next); } } } /** * @brief dump the truth table of given bbdd * * @param output pointer to the root of a bbdd for which the truth table * should be printed * @return string of the output tt */ std::string dump_tt(bbdd_node_t *output) { std::vector tt(std::pow(2, this->num_inputs), false); std::vector var_rel; recursive_dump_tt(output, var_rel, this->num_inputs, tt); for (int i = 0; i < tt.size(); i++) { for (int j = 0; j < this->num_inputs; j++) { printf("%d", get_ith_bit(i, this->num_inputs, j)); } printf(" | %s\n", tt[i] ? "1" : "0"); } std::string out_string = ""; for (int i = 0; i < tt.size(); i++) { out_string += tt[i] ? "1" : "0"; } return out_string; } /** * @brief dump truth table for output string name * * @param output name of the output in the output map * @return string of the tt, empty if output name does not exist in output map */ std::string dump_tt(std::string output) { std::printf("Truth table of output %s\n", output.c_str()); for (output_map_t out_map : this->output_map) { if (out_map.output == output) { return dump_tt(out_map.bbdd); } } return ""; } /** * @brief dump bbdd of given output into a dot file format * * @param filename name of the file in which the output will be dumped * @param output name of the output which should be dumped, dot file only * consists of terminal node if output name is not in the output map */ void dump_dot(std::string filename, std::string output) { std::ofstream dot_file(filename); dot_file << "graph bbdd {\n"; // terminal nodes dot_file << "\t0 [shape=square]\n"; dot_file << "\t1 [shape=square]"; bbdd_node_t *root_node; for (output_map_t map : output_map) { if (map.output == output) { root_node = map.bbdd; break; } } node_index_t root = recursive_dump_dot(dot_file, root_node); clear_marks(root_node); dot_file << "\n\t" << free_pos + 1 << " [shape=plaintext, label=\"" << output << "\"]\n"; dot_file << "\t" << free_pos + 1 << " -- " << root_node->index << "\n"; dot_file << "}\n"; } /** * @brief dump all bbdd nodes that have a defined output of the module into a * dot file format * * @param filename name in which the design should be printed to */ void dump_dot(std::string filename) { std::ofstream dot_file(filename); dot_file << "graph bbdd {\n"; // terminal nodes dot_file << "\t0 [shape=square]\n"; dot_file << "\t1 [shape=square]\n"; // insert nodes for (uint64_t i = 2; i < free_pos; i++) { table_entry_t entry = entries[i]; if (entry.node.cvo_lvl.sv != INT_MAX) { dot_file << "\n" << i << " [label=\"" << entry.node.ref << "\n" << i << ": " << entry.node.cvo_lvl.pv << "," << entry.node.cvo_lvl.sv << "\"]"; } else { dot_file << "\n" << i << " [label=\"" << entry.node.ref << "\n" << i << ": " << entry.node.cvo_lvl.pv << ",1" << "\"]"; } dot_file << "\t" << i << " -- " << entry.node.neq_child << "[label=<>, " "style=\"dashed\"]\n"; dot_file << "\t" << i << " -- " << entry.node.eq_child << "[label=\"=\"]\n"; } for (output_map_t map : output_map) { dot_file << "\n" << map.output << " [shape=plaintext, label=\"" << map.output << "\"]"; dot_file << "\t" << map.output << " -- " << map.bbdd->index << "\n"; } dot_file << "}\n"; } /** * @brief same as previous dump_dot function but it uses a signal map that * maps primary and secondary variables to human readable strings * * @param filename in which the design should be written to * @param signal_map maps indices of primary and secondary variables to human * readable strings */ void dump_dot(std::string filename, std::vector signal_map) { std::ofstream dot_file(filename); dot_file << "graph bbdd {\n"; // terminal nodes dot_file << "\t0 [shape=square]"; dot_file << "\t1 [shape=square]"; // insert nodes for (uint64_t i = 2; i < free_pos; i++) { table_entry_t entry = entries[i]; if (entry.node.ref == 0) { continue; } if (entry.node.cvo_lvl.sv != INT_MAX) { dot_file << "\n" << i << " [label=\"" << entry.node.ref << "\n" << i << ": " << signal_map[entry.node.cvo_lvl.pv - 2] << "," << signal_map[entry.node.cvo_lvl.sv - 2] << "\"]"; } else { dot_file << "\n" << i << " [label=\"" << entry.node.ref << "\n" << i << ": " << signal_map[entry.node.cvo_lvl.pv - 2] << ",1" << "\"]"; } dot_file << "\t" << i << " -- " << entry.node.neq_child << "[label=<>, " "style=\"dashed\"]\n"; dot_file << "\t" << i << " -- " << entry.node.eq_child << "[label=\"=\"]\n"; } for (output_map_t map : output_map) { dot_file << "\n" << map.output << " [shape=plaintext, label=\"" << map.output << "\"]"; dot_file << "\t" << map.output << " -- " << map.bbdd->index << "\n"; } dot_file << "}\n"; } /** * @brief dump the current module into blif file format * * @param filename name of the file in which the diagrams should be dumped * into, only outputs are considered that are present in the output map */ void write_blif(std::string filename) { std::ofstream blif_file(filename); blif_file << ".model " + this->module_name + "\n"; blif_file << ".inputs"; for (int i = 0; i < this->signal_map.size(); i++) { blif_file << " " << this->signal_map[i]; } blif_file << "\n.outputs"; for (output_map_t output : this->output_map) { blif_file << " " << output.output; } blif_file << "\n.names $true\n1\n"; blif_file << ".names $false\n"; for (output_map_t map : this->output_map) { if (IS_TERM(map.bbdd->index)) { if (map.bbdd->index == 0) { blif_file << ".names " << map.output << "\n"; } else { blif_file << ".names " << map.output << "\n1\n"; } } else if (MARKED(map.bbdd)) { blif_file << ".names " << (GET_INDEX(map.bbdd)) << " " << map.output << "\n1 1\n"; } else { // write_blif_recursive(blif_file, map.bbdd, cover.signal_map, true); // blif_file << map.output << "\n0-1 1\n11- 1\n"; write_blif_recursive_muxxor(blif_file, map.bbdd, signal_map, true); blif_file << map.output << "\n00-1 1\n011- 1\n101- 1\n11-1 1\n"; } } blif_file << ".end\n"; } + void write_blif(std::string filename, std::string module_name, std::vector signal_map, unsigned int input_size) { + std::ofstream blif_file(filename); + blif_file << ".model " + module_name + "\n"; + blif_file << ".inputs"; + for (int i = 0; i < signal_map.size(); i++) { + blif_file << " " << signal_map[i]; + if (i + 1 == input_size) { + blif_file << "\n.outputs"; + } + } + blif_file << "\n.names $true\n1\n"; + blif_file << ".names $false\n"; + for (output_map_t map : output_map) { + if (IS_TERM(map.bbdd->index)) { + if (map.bbdd->index == 0) { + blif_file << ".names " << map.output << "\n"; + } else { + blif_file << ".names " << map.output << "\n1\n"; + } + } else if (MARKED(map.bbdd)) { + blif_file << ".names " << (GET_INDEX(map.bbdd)) << " " << map.output + << "\n1 1\n"; + } else { + write_blif_recursive_muxxor(blif_file, map.bbdd, signal_map, true); + blif_file << map.output << "\n00-1 1\n011- 1\n101- 1\n11-1 1\n"; + } + } + blif_file << ".end\n"; + } + #ifdef CACHE_STATS void print_cache_stats() { printf( "[INFO] CACHE STATS: inserts: %d, hits: %d, misses %d, max chain: %d\n", cache_stats.inserts, cache_stats.hits, cache_stats.misses, cache_stats.chain); } void dump_cache_stats(std::string path) { std::ofstream csv_file(path); csv_file << "inserts;hits;misses;max_chain;extend_lookups;extend_hits;" "merge_lookups;merge_hits\n"; csv_file << std::to_string(cache_stats.inserts) << ";" << std::to_string(cache_stats.hits) << ";" << std::to_string(cache_stats.misses) << ";" << std::to_string(cache_stats.chain) << ";" << std::to_string(cache_stats.extend_lookups) << ";" << std::to_string(cache_stats.extend_hits) << ";" << std::to_string(cache_stats.merge_lookups) << ";" << std::to_string(cache_stats.merge_hits) << "\n"; csv_file.close(); } #endif /** * @brief get maximum tree height of a bbdd * * @param root root node of bbdd node for which the height should be * calculated * @param height intermediate values used for the recursion * @return maximum height of the current bbdd node to any terminal node */ uint32_t get_tree_height(bbdd_node_t *root, uint32_t height) { if (IS_TERM(root->index)) { return 0; } bbdd_node_t *neq = get_node_p(root->neq_child); bbdd_node_t *eq = get_node_p(root->eq_child); return std::max(get_tree_height(neq, height) + 1, get_tree_height(eq, height) + 1); } /** * @brief gets maximum tree height of a bbdd * * @param node root node of bbdd node for which the height should be * calculated * @return maximum height of the current bbdd node to any terminal node */ uint32_t get_tree_height(bbdd_node_t *node) { return get_tree_height(node, 0); } /** * @brief return the maximum tree height of all bbdds registered in the output * map * * @return maximum tree height of all bbdds in the design */ uint32_t get_max_height() { uint32_t max_height = -1; uint32_t current_height; for (output_map_t out_map : output_map) { current_height = get_tree_height(out_map.bbdd); if (current_height > max_height) { max_height = current_height; } } return max_height; } /** * @brief return the sum of all maximum tree heights of all bbdd nodes that * have registered an output in the output map * * @return sum of all maximum tree heights */ uint32_t get_total_height() { uint32_t sum = 0; for (output_map_t out_map : output_map) { sum += get_tree_height(out_map.bbdd); } return sum; } /** * @brief reorders a bbdd based on two variables that are swapped * * @param node root node to the bbdd which should be reordered * @param b first variable * @param c second variable * @return newly created bbdd based on the swapped varaibles inserted into the * hash table */ bbdd_node_t *reorder_bbdd(bbdd_node_t *node, node_index_t b, node_index_t c) { #ifdef DEBUG_REORDER printf("reorder: "); dump_node(node); printf("\n"); #endif if (IS_TERM(node->index)) { return node; } bbdd_node_t *neq_child = get_node_p(node->neq_child); bbdd_node_t *eq_child = get_node_p(node->eq_child); bbdd_node_t *new_neq, *new_eq, *new_neq_neq, *new_neq_eq, *new_eq_neq, *new_eq_eq; bbdd_node_t *neq_neq_child, *neq_eq_child, *eq_neq_child, *eq_eq_child; node_index_t nnn, nne, nen, nee, enn, ene, een, eee; uint32_t nn_sv, ne_sv, en_sv, ee_sv; // b no SV if (node->cvo_lvl.pv == b) { // c not present in this bbdd if (node->cvo_lvl.sv != c) { return node; } // NEQ-Child if (neq_child->cvo_lvl.pv != c) { new_neq = neq_child; } else { new_neq = insert_node({{b, neq_child->cvo_lvl.sv}, neq_child->eq_child, neq_child->neq_child}); } // EQ-Child if (eq_child->cvo_lvl.pv != c) { new_eq = eq_child; } else { new_eq = insert_node({{b, eq_child->cvo_lvl.sv}, eq_child->neq_child, eq_child->eq_child}); } assert(new_neq->cvo_lvl.sv == INT_MAX || POS(new_neq->cvo_lvl.pv, cvo) < POS(new_neq->cvo_lvl.sv, cvo)); assert(new_eq->cvo_lvl.sv == INT_MAX || POS(new_eq->cvo_lvl.pv, cvo) < POS(new_eq->cvo_lvl.sv, cvo)); assert(POS(c, cvo) < POS(b, cvo)); return insert_node({{c, b}, new_neq->index, new_eq->index}); } // b SV if (node->cvo_lvl.sv == b) { // NEQ-Child if (neq_child->cvo_lvl.pv == b) { if (neq_child->cvo_lvl.sv != c) { nnn = nee = neq_child->eq_child; nne = nen = neq_child->neq_child; nn_sv = ne_sv = neq_child->cvo_lvl.sv; } else { // c SV in neq_child neq_neq_child = get_node_p(neq_child->neq_child); neq_eq_child = get_node_p(neq_child->eq_child); // full neq neq if (neq_neq_child->cvo_lvl.pv == c) { nnn = neq_neq_child->neq_child; nne = neq_neq_child->eq_child; nn_sv = neq_neq_child->cvo_lvl.sv; // c no neq neq PV } else { nnn = nne = neq_neq_child->index; nn_sv = neq_neq_child->cvo_lvl.pv; } // full neq eq if (neq_eq_child->cvo_lvl.pv == c) { nen = neq_eq_child->neq_child; nee = neq_eq_child->eq_child; ne_sv = neq_eq_child->cvo_lvl.sv; // c no neq eq PV } else { nen = nee = neq_eq_child->index; ne_sv = neq_eq_child->cvo_lvl.pv; } } } else { // b no PV in neq_child if (neq_child->cvo_lvl.pv == c) { // c PV in neq_child nnn = nen = neq_child->neq_child; nne = nee = neq_child->eq_child; nn_sv = ne_sv = neq_child->cvo_lvl.sv; } else { nnn = nne = nen = nee = neq_child->index; nn_sv = ne_sv = neq_child->cvo_lvl.pv; } } // EQ-Child if (eq_child->cvo_lvl.pv == b) { if (eq_child->cvo_lvl.sv != c) { ene = een = eq_child->neq_child; enn = eee = eq_child->eq_child; en_sv = ee_sv = eq_child->cvo_lvl.sv; } else { // c is sv in eq_child eq_neq_child = get_node_p(eq_child->neq_child); eq_eq_child = get_node_p(eq_child->eq_child); if (eq_neq_child->cvo_lvl.pv == c) { enn = eq_neq_child->neq_child; ene = eq_neq_child->eq_child; en_sv = eq_neq_child->cvo_lvl.sv; } else { enn = ene = eq_neq_child->index; en_sv = eq_neq_child->cvo_lvl.pv; } if (eq_eq_child->cvo_lvl.pv == c) { een = eq_eq_child->neq_child; eee = eq_eq_child->eq_child; ee_sv = eq_eq_child->cvo_lvl.sv; } else { een = eee = eq_eq_child->index; ee_sv = eq_eq_child->cvo_lvl.pv; } } } else { // b is not pv in eq_child if (eq_child->cvo_lvl.pv == c) { enn = een = eq_child->neq_child; ene = eee = eq_child->eq_child; en_sv = ee_sv = eq_child->cvo_lvl.sv; } else { enn = ene = een = eee = eq_child->index; en_sv = ee_sv = eq_child->cvo_lvl.pv; } } // create new bbdd // new neq assert(en_sv == INT_MAX || ene == enn || POS(b, cvo) < POS(en_sv, cvo)); assert(ne_sv == INT_MAX || nen == nee || POS(b, cvo) < POS(ne_sv, cvo)); assert(POS(c, cvo) < POS(b, cvo)); new_neq_neq = insert_node({{b, en_sv}, ene, enn}); new_neq_eq = insert_node({{b, ne_sv}, nen, nee}); new_neq = insert_node({{c, b}, new_neq_neq->index, new_neq_eq->index}); // new eq assert(nn_sv == INT_MAX || nne == nnn || POS(b, cvo) < POS(nn_sv, cvo)); assert(ee_sv == INT_MAX || een == eee || POS(b, cvo) < POS(ee_sv, cvo)); assert(POS(c, cvo) < POS(b, cvo)); new_eq_neq = insert_node({{b, nn_sv}, nne, nnn}); new_eq_eq = insert_node({{b, ee_sv}, een, eee}); new_eq = insert_node({{c, b}, new_eq_neq->index, new_eq_eq->index}); // new root assert(POS(node->cvo_lvl.pv, cvo) < POS(c, cvo)); return insert_node( {{node->cvo_lvl.pv, c}, new_neq->index, new_eq->index}); } new_neq = reorder_bbdd(get_node_p(node->neq_child), b, c); new_eq = reorder_bbdd(get_node_p(node->eq_child), b, c); if (!(node->cvo_lvl.sv == INT_MAX || POS(node->cvo_lvl.pv, cvo) < POS(node->cvo_lvl.sv, cvo))) { dump_node(node); std::cout << "\n"; } assert(node->cvo_lvl.sv == INT_MAX || POS(node->cvo_lvl.pv, cvo) < POS(node->cvo_lvl.sv, cvo)); return insert_node({{node->cvo_lvl}, new_neq->index, new_eq->index}); } /** * @brief return the total number of nodes in a bbdd * * @return total number od nodes in a bbdd */ uint32_t get_total_number_nodes() { uint32_t count = 0; for (output_map_t out_map : output_map) { count += get_number_nodes_recursive(out_map.bbdd); } for (output_map_t out_map : output_map) { clear_marks(out_map.bbdd); } return count; } /** * @brief dump information stored in the output map: name of the output and * the index of the bbdd node that is the root noddump information stored in * the output map: name of the output and the index of the bbdd node that is * the root node for that output */ void dump_outputs() { for (output_map_t out_map : output_map) { printf("Output: %s: ", out_map.output.c_str()); dump_node(out_map.bbdd); printf("\n"); } } /** * @brief swap two inputs in the variable ordering and reorder bbdd based on the new ordering * * @param root root bbdd node that should be reordered after variable swap * @param b first variable * @param c second variable * @return newly created bbdd node based on new variable order */ bbdd_node_t *swap_positions(bbdd_node_t *root, node_index_t b, node_index_t c) { // assert(POS(b, cvo) + 1 == POS(c, cvo)); assert(b + 1 == c); node_index_t temp = (*cvo)[b].in; (*cvo)[b].in = (*cvo)[c].in; (*cvo)[c].in = temp; (*cvo)[(*cvo)[b].in % num_inputs].pos = b; (*cvo)[(*cvo)[c].in % num_inputs].pos = c; return reorder_bbdd(root, VAR(c, cvo), VAR(b, cvo)); } /** * @brief reduce size of the bbdd node based on reduction rules * * @param f root node to bbdd that should be reduced * @return pointer to reduced bbdd */ bbdd_node_t *reduce_bbdd(bbdd_node_t *f) { if (IS_TERM(f->index)) { return f; } bbdd_node_t *child_neq = get_node_p(f->neq_child), *child_eq = get_node_p(f->eq_child); bbdd_node_t *new_neq, *new_eq, new_root; new_neq = reduce_bbdd(child_neq); new_eq = reduce_bbdd(child_eq); if (new_neq->index == new_eq->index) { #ifdef DEBUG_BBDD printf("[INFO] REDUCE: node %d\n", f->index); #endif return new_neq; } if (!(IS_TERM(new_neq->index)) && !(IS_TERM(new_eq->index)) && new_neq->cvo_lvl.pv == new_eq->cvo_lvl.pv && new_neq->cvo_lvl.sv == new_eq->cvo_lvl.sv && f->cvo_lvl.sv == new_neq->cvo_lvl.pv && new_neq->neq_child == new_eq->eq_child && new_neq->eq_child == new_eq->neq_child) { return insert_node({{f->cvo_lvl.pv, new_neq->cvo_lvl.sv}, new_neq->eq_child, new_neq->neq_child}); } assert(f->cvo_lvl.sv == INT_MAX || POS(f->cvo_lvl.pv, cvo) < POS(f->cvo_lvl.sv, cvo)); return insert_node({f->cvo_lvl, new_neq->index, new_eq->index}); } /** * @brief swap two adjacent variables in ordering and reorder all bbdd that have a registered output * * @param pos_b position of first variable * @param pos_c position of second variable */ void swap_all_positions(node_index_t pos_b, node_index_t pos_c) { node_index_t var_b = (*cvo)[pos_b].in; node_index_t var_c = (*cvo)[pos_c].in; swap_variable_order(pos_b, pos_c); for (uint32_t i = 0; i < output_map.size(); i++) { output_map[i].bbdd = reduce_bbdd(reorder_bbdd(output_map[i].bbdd, var_b, var_c)); } } };