No OneTemporary
Actions

Authored By

Unknown

Size

45 KB

Referenced Files

None

Subscribers

None

View Options

	diff --git a/include/unique_table.hpp b/include/unique_table.hpp
	index 6c29664..d4ac98e 100644
	--- a/include/unique_table.hpp
	+++ b/include/unique_table.hpp
	@@ -1,1279 +1,1293 @@
	// Copyright 2025 Oliver Theimer
	#pragma once
	#include <algorithm>
	#include <cassert>
	#include <climits>
	#include <cmath>
	#include <cstdint>
	#include <cstdio>
	#include <fstream>
	#include <iostream>
	#include <string>
	#include <unordered_map>
	#include <vector>

	#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<node_index_t> 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=<<FONT POINT-SIZE=\"14\">≠</FONT>>]\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<variable_relation_t> var_rel,
	node_index_t inputs, std::vector<bool> &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<variable_relation_t> var_rel,
	node_index_t inputs, std::vector<bool> &tt) {
	std::vector<variable_relation_t> neq_rel = var_rel;
	std::vector<variable_relation_t> 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<std::string> 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
	+ * @param wire_prefix prepended to every internal wire name. Node indices are
	+ * only unique within one table, so when several tables are written into the
	+ * same module a per table prefix is required to keep their wires apart. Pass
	+ * an empty string for a module that comes from a single table.
	* @return bbdd node index of the current bbdd node only used during recursion
	*/
	- uint32_t write_blif_recursive_muxxor(std::ofstream &blif_file,
	+ uint32_t write_blif_recursive_muxxor(std::ostream &blif_file,
	bbdd_node_t *node,
	- std::vector<std::string> signal_map,
	- bool output) {
	+ std::vector<std::string> const &signal_map,
	+ bool output,
	+ std::string const &wire_prefix = "") {
	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);
	+ blif_file, get_node_p(node->neq_child), signal_map, false, wire_prefix);
	uint32_t right_child = write_blif_recursive_muxxor(
	- blif_file, get_node_p(node->eq_child), signal_map, false);
	+ blif_file, get_node_p(node->eq_child), signal_map, false, wire_prefix);
	// 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);
	+ in1 = wire_prefix + std::to_string(right_child);
	}
	if (IS_TERM(left_child)) {
	in0 = left_child == 0 ? "$false" : "$true";
	} else {
	- in0 = std::to_string(left_child);
	+ in0 = wire_prefix + 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 << wire_prefix << 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_t> output_map;
	std::vector<std::string> signal_map;
	cvo_t *cvo;
	uint32_t num_inputs;
	std::unordered_map<merge_key, node_index_t, merge_hash> computed_table;
	std::unordered_map<extend_key, bbdd_node_ppair_t, extend_hash> 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<uint64_t> inputs, cvo_init_t cvo_opt,
	std::vector<node_index_t> input_cvo = std::vector<node_index_t>()) {
	cvo = reinterpret_cast<cvo_t *>(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<std::string> 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<table_entry_t *>(
	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<bool> tt(std::pow(2, this->num_inputs), false);
	std::vector<variable_relation_t> 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=<<FONT POINT-SIZE=\"14\">≠</FONT>>, "
	"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<std::string> 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=<<FONT POINT-SIZE=\"14\">≠</FONT>>, "
	"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";
	- }
	- }
	+ write_blif_body(blif_file, this->signal_map);
	blif_file << ".end\n";
	}

	void write_blif(std::string filename, std::string module_name, std::vector<std::string> 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";
	+ write_blif_body(blif_file, signal_map);
	+ blif_file << ".end\n";
	+ }
	+
	+ /**
	+ * @brief writes the gates of every registered output, without a file header
	+ *
	+ * Emits only the `.names` blocks that realise the outputs in the output map,
	+ * so that the diagrams of several tables can be written into a single blif
	+ * module. The caller owns the file and is responsible for the `.model`,
	+ * `.inputs`, `.outputs`, the `$true`/`$false` constants and the `.end`.
	+ *
	+ * This is what makes a partitioned run possible: every block of a partition
	+ * is converted in its own table, and each table numbers its nodes from 2
	+ * again, so the internal wire names of two blocks would collide in a shared
	+ * module. Giving each block a distinct wire_prefix keeps them apart.
	+ *
	+ * @param blif_file stream the gates should be appended to
	+ * @param signal_map maps a bbdd variable id minus 2 to a human readable name,
	+ * used for the leaves of the diagrams
	+ * @param wire_prefix prepended to every internal wire name of this table
	+ */
	+ void write_blif_body(std::ostream &blif_file,
	+ std::vector<std::string> const &signal_map,
	+ std::string const &wire_prefix = "") {
	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";
	+ blif_file << ".names " << wire_prefix << (GET_INDEX(map.bbdd)) << " "
	+ << map.output << "\n1 1\n";
	} else {
	- write_blif_recursive_muxxor(blif_file, map.bbdd, signal_map, true);
	+ write_blif_recursive_muxxor(blif_file, map.bbdd, signal_map, true,
	+ wire_prefix);
	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));
	}
	}
	};

File Metadata

Mime Type: text/x-diff
Expires: Tue, Oct 27, 8:35 PM (17 h, 6 m)
Storage Engine: blob
Storage Format: Raw Data
Storage Handle: 410190
Default Alt Text: (45 KB)

No OneTemporaryActions

View Options

File Metadata

Event Timeline

No OneTemporary
Actions