added netlist preprocessing info, small change to dana pass and other…

… stuff.

plugins/boolean_influence/include/boolean_influence/plugin_boolean_influence.h

@@ -69,11 +69,20 @@ namespace hal
          *
          * @param[in] bf - The Boolean function.
          * @param[in] num_evaluations - The amount of evaluations that are performed for each input variable.
-         * @param[in] unique_identifier - A unique identifier that is applied to file names to prevent collisions during multi-threading.
          * @returns A map from the variables that appear in the function to their Boolean influence on said function on success, an error otherwise.
          */
         static Result<std::unordered_map<std::string, double>> get_boolean_influence_with_hal_boolean_function_class(const BooleanFunction& bf, const u32 num_evaluations);
 
+        /**
+         * Generates the Boolean influence of each input variable of a Boolean function using z3 expressions and substitutions/simplifications only.
+         * The function is slower, but can be better used in multithreading enviroment.
+         *
+         * @param[in] bf - The Boolean function.
+         * @param[in] num_evaluations - The amount of evaluations that are performed for each input variable.
+         * @returns A map from the variables that appear in the function to their Boolean influence on said function on success, an error otherwise.
+         */
+        static Result<std::unordered_map<std::string, double>> get_boolean_influence_with_z3_expr(const BooleanFunction& bf, const u32 num_evaluations);
+
         /**
          * Generates the Boolean influence of each input variable of a Boolean function.
          *

plugins/boolean_influence/src/plugin_boolean_influence.cpp

@@ -31,10 +31,8 @@ namespace hal
 
     namespace
     {
-        static unsigned long x = 123456789, y = 362436069, z = 521288629;
-
         // period 2^96-1
-        unsigned long xorshf96(void)
+        unsigned long xorshf96(u64& x, u64& y, u64& z)
         {
             unsigned long t;
 
@@ -49,6 +47,7 @@ namespace hal
 
             return z;
         }
+
         void add_inputs(Gate* gate, std::unordered_set<Gate*>& gates)
         {
             if (!gate->get_type()->has_property(GateTypeProperty::combinational) || gate->is_vcc_gate() || gate->is_gnd_gate())
@@ -187,7 +186,6 @@ int main(int argc, char *argv[]) {
     Result<std::unordered_map<std::string, double>>
         BooleanInfluencePlugin::get_boolean_influence_internal(const z3::expr& expr, const u32 num_evaluations, const bool deterministic, const std::string& unique_identifier)
     {
-        bool use_z3                   = true;
         const auto to_replacement_var = [](const u32 var_idx) -> std::string { return "var_" + std::to_string(var_idx); };
 
         const auto extract_index = [](const std::string& var) -> Result<u32> {
@@ -481,6 +479,8 @@ int main(int argc, char *argv[]) {
         std::unordered_map<std::string, double> influences;
         std::set<std::string> variables = bf.get_variable_names();
 
+        u64 x = 123456789, y = 362436069, z = 521288629;
+
         for (const auto& var : variables)
         {
             u32 count = 0;
@@ -495,7 +495,7 @@ int main(int argc, char *argv[]) {
                         continue;
                     }
 
-                    BooleanFunction::Value random_value = (xorshf96() % 2) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO;
+                    BooleanFunction::Value random_value = (xorshf96(x, y, z) % 2) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO;
                     values.insert({var_to_set, random_value});
                 }
 
@@ -530,6 +530,161 @@ int main(int argc, char *argv[]) {
         return OK(influences);
     }
 
+    Result<std::unordered_map<std::string, double>> BooleanInfluencePlugin::get_boolean_influence_with_z3_expr(const BooleanFunction& bf, const u32 num_evaluations)
+    {
+        std::unordered_map<std::string, double> influences;
+        std::set<std::string> variables = bf.get_variable_names();
+
+        auto ctx   = z3::context();
+        auto z3_bf = z3_utils::from_bf(bf, ctx);
+
+        u64 x = 123456789, y = 362436069, z = 521288629;
+
+        for (const auto& var : variables)
+        {
+            const auto var_expr = ctx.bv_const(var.c_str(), 1);
+
+            u32 count = 0;
+            for (unsigned long long i = 0; i < num_evaluations; i++)
+            {
+                z3::expr_vector from_vec(ctx);
+                z3::expr_vector to_vec(ctx);
+
+                // build value
+                for (const auto& var_to_set : variables)
+                {
+                    if (var == var_to_set)
+                    {
+                        continue;
+                    }
+
+                    const auto var_to_set_expr = ctx.bv_const(var_to_set.c_str(), 1);
+
+                    auto random_value = (xorshf96(x, y, z) % 2) ? ctx.bv_val(1, 1) : ctx.bv_val(0, 1);
+
+                    from_vec.push_back(var_to_set_expr);
+                    to_vec.push_back(random_value);
+                }
+
+                auto z3_bf_substitute = z3_bf.substitute(from_vec, to_vec).simplify();
+
+                z3::expr_vector from_vec_var(ctx);
+                z3::expr_vector to_vec_one(ctx);
+                z3::expr_vector to_vec_zero(ctx);
+
+                from_vec_var.push_back(var_expr);
+                to_vec_one.push_back(ctx.bv_val(1, 1));
+                to_vec_zero.push_back(ctx.bv_val(0, 1));
+
+                // evaluate 1
+                const auto res_1 = z3_bf_substitute.substitute(from_vec_var, to_vec_one).simplify();
+                if (!res_1.is_numeral())
+                {
+                    std::cout << res_1 << std::endl;
+                    return ERR("cannot determine boolean influence of variabel " + var + ": failed to simplify to a constant");
+                }
+
+                // evaluate 0
+                const auto res_2 = z3_bf_substitute.substitute(from_vec_var, to_vec_zero).simplify();
+                if (!res_2.is_numeral())
+                {
+                    std::cout << res_2 << std::endl;
+                    return ERR("cannot determine boolean influence of variabel " + var + ": failed to simplify to a constant");
+                }
+
+                const auto r1 = res_1.get_numeral_uint64();
+                const auto r2 = res_2.get_numeral_uint64();
+
+                if (r1 != r2)
+                {
+                    count++;
+                }
+            }
+            double cv = (double)(count) / (double)(num_evaluations);
+            influences.insert({var, cv});
+        }
+
+        return OK(influences);
+    }
+
+    /*
+    Result<std::unordered_map<std::string, double>> BooleanInfluencePlugin::get_boolean_influence_with_z3_expr(const BooleanFunction& bf, const u32 num_evaluations)
+    {
+        std::unordered_map<std::string, double> influences;
+        std::set<std::string> variables = bf.get_variable_names();
+
+        auto ctx   = z3::context();
+        auto z3_bf = z3_utils::from_bf(bf, ctx);
+        auto s     = z3::solver(ctx);
+
+        u64 x = 123456789, y = 362436069, z = 521288629;
+
+        for (const auto& var : variables)
+        {
+            const auto var_expr = ctx.bv_const(var.c_str(), 1);
+
+            u32 count = 0;
+            for (unsigned long long i = 0; i < num_evaluations; i++)
+            {
+                s.push();
+                // build value
+                for (const auto& var_to_set : variables)
+                {
+                    if (var == var_to_set)
+                    {
+                        continue;
+                    }
+
+                    const auto var_to_set_expr = ctx.bv_const(var_to_set.c_str(), 1);
+
+                    auto random_value = (xorshf96(x, y, z) % 2) ? ctx.bv_val(1, 1) : ctx.bv_val(0, 1);
+
+                    s.add(var_to_set_expr == random_value);
+                }
+
+                // evaluate 1
+                s.push();
+                s.add(var_expr == ctx.bv_val(1, 1));
+                s.check();
+                const auto m_1   = s.get_model();
+                const auto res_1 = m_1.eval(z3_bf);
+                if (!res_1.is_numeral())
+                {
+                    std::cout << res_1 << std::endl;
+                    return ERR("cannot determine boolean influence of variabel " + var + ": failed to simplify to a constant");
+                }
+                s.pop();
+
+                // evaluate 0
+                s.push();
+                s.add(var_expr == ctx.bv_val(0, 1));
+                s.check();
+                const auto m_2   = s.get_model();
+                const auto res_2 = m_2.eval(z3_bf);
+                if (!res_2.is_numeral())
+                {
+                    std::cout << res_2 << std::endl;
+                    return ERR("cannot determine boolean influence of variabel " + var + ": failed to simplify to a constant");
+                }
+                s.pop();
+
+                const auto r1 = res_1.get_numeral_uint64();
+                const auto r2 = res_2.get_numeral_uint64();
+
+                if (r1 != r2)
+                {
+                    count++;
+                }
+                s.pop();
+            }
+            double cv = (double)(count) / (double)(num_evaluations);
+            influences.insert({var, cv});
+        }
+
+        return OK(influences);
+    }
+    */
+
     Result<std::unordered_map<std::string, double>> BooleanInfluencePlugin::get_boolean_influence(const z3::expr& expr, const u32 num_evaluations, const std::string& unique_identifier)
     {
         return get_boolean_influence_internal(expr, num_evaluations, false, unique_identifier);

plugins/dataflow_analysis/src/processing/passes/group_by_successor_predecessor_known_groups.cpp

@@ -20,6 +20,7 @@ namespace hal
 
                 /* check characteristics */
                 std::map<std::set<u32>, std::list<u32>> characteristics_map;
+                std::vector<u32> groups_with_no_characteristics;
                 for (const auto& [group_id, group] : state->gates_of_group)
                 {
                     std::set<u32> characteristics_of_group;
@@ -35,7 +36,14 @@ namespace hal
                         characteristics_of_group.insert(predecessing_known_group.begin(), predecessing_known_group.end());
                     }
 
-                    characteristics_map[characteristics_of_group].push_back(group_id);
+                    if (characteristics_of_group.empty())
+                    {
+                        groups_with_no_characteristics.push_back(group_id);
+                    }
+                    else
+                    {
+                        characteristics_map[characteristics_of_group].push_back(group_id);
+                    }
                 }
 
                 /* check if merge is allowed */
@@ -68,6 +76,12 @@ namespace hal
                     }
                 }
 
+                /* add all groups with no characteristics as singleton merge set */
+                for (const auto& group_id : groups_with_no_characteristics)
+                {
+                    merge_sets.push_back({group_id});
+                }
+
                 /* merge groups */
                 u32 id_counter = -1;
                 for (const auto& groups_to_merge : merge_sets)

plugins/netlist_preprocessing/include/netlist_preprocessing/helper_lib.h

@@ -8,15 +8,15 @@ namespace hal
     {
         std::string yosys_helper_lib = "";
         yosys_helper_lib += "// GND\n";
-        yosys_helper_lib += "module GND (Y);\n";
-        yosys_helper_lib += "output Y;\n";
-        yosys_helper_lib += "assign Y = 1\'b0;\n";
+        yosys_helper_lib += "module GND (G);\n";
+        yosys_helper_lib += "output G;\n";
+        yosys_helper_lib += "assign G = 1\'b0;\n";
         yosys_helper_lib += "endmodule\n";
         yosys_helper_lib += "\n";
         yosys_helper_lib += "// VCC\n";
-        yosys_helper_lib += "module VCC (Y);\n";
-        yosys_helper_lib += "output Y;\n";
-        yosys_helper_lib += "assign Y = 1\'b1;\n";
+        yosys_helper_lib += "module VCC (P);\n";
+        yosys_helper_lib += "output P;\n";
+        yosys_helper_lib += "assign P = 1\'b1;\n";
         yosys_helper_lib += "endmodule\n";
         yosys_helper_lib += "\n";
         yosys_helper_lib += "// BUF\n";

plugins/netlist_preprocessing/include/netlist_preprocessing/plugin_netlist_preprocessing.h

@@ -265,5 +265,10 @@ namespace hal
          * return OK on success, an error otherwise.
         */
         static Result<std::monostate> parse_def_file(Netlist* nl, const std::filesystem::path& def_file);
+
+        /**
+         * Create modules from large gates like RAMs and DSPs with the option to concat mutliple gate pingroups to larger consecutive pin groups
+         */
+        static Result<std::vector<Module*>> create_multi_bit_gate_modules(Netlist* nl, const std::map<std::string, std::map<std::string, std::vector<std::string>>>& concatinated_pin_groups);
     };
 }    // namespace hal

plugins/netlist_preprocessing/python/python_bindings.cpp

@@ -598,6 +598,31 @@ namespace hal
                 :rtype: bool
             )");
 
+        py_netlist_preprocessing.def_static(
+            "create_multi_bit_gate_modules",
+            [](Netlist* nl, const std::map<std::string, std::map<std::string, std::vector<std::string>>>& concatinated_pin_groups) -> std::vector<Module*> {
+                auto res = NetlistPreprocessingPlugin::create_multi_bit_gate_modules(nl, concatinated_pin_groups);
+                if (res.is_ok())
+                {
+                    return res.get();
+                }
+                else
+                {
+                    log_error("python_context", "{}", res.get_error().get());
+                    return {};
+                }
+            },
+            py::arg("nl"),
+            py::arg("concatinated_pin_groups"),
+            R"(
+                Create modules from large gates like RAMs and DSPs with the option to concat mutliple gate pingroups to larger consecutive pin groups.
+
+                :param hal_py.Netlist nl: The netlist to operate on. 
+                :param  concatinated_pin_groups: 
+                :returns: ``True`` on success, ``False`` otherwise.
+                :rtype: bool
+            )");
+
 #ifndef PYBIND11_MODULE
         return m.ptr();
 #endif    // PYBIND11_MODULE

plugins/netlist_preprocessing/src/plugin_netlist_preprocessing.cpp

@@ -1815,4 +1815,61 @@ namespace hal
         return OK({});
     }
 
+    Result<std::vector<Module*>> NetlistPreprocessingPlugin::create_multi_bit_gate_modules(Netlist* nl,
+                                                                                           const std::map<std::string, std::map<std::string, std::vector<std::string>>>& concatinated_pin_groups)
+    {
+        std::vector<Module*> all_modules;
+        for (const auto& [gt_name, pin_groups] : concatinated_pin_groups)
+        {
+            for (const auto& g : nl->get_gates([&gt_name](const auto& g) { return g->get_type()->get_name() == gt_name; }))
+            {
+                auto m = nl->create_module("module_" + g->get_name(), g->get_module(), {g});
+
+                for (const auto& [module_pg_name, gate_pg_names] : pin_groups)
+                {
+                    std::vector<ModulePin*> module_pins;
+                    for (const auto& gate_pg_name : gate_pg_names)
+                    {
+                        const auto& gate_pg            = g->get_type()->get_pin_group_by_name(gate_pg_name);
+                        std::vector<GatePin*> pin_list = gate_pg->get_pins();
+                        if (!gate_pg->is_ascending())
+                        {
+                            std::reverse(pin_list.begin(), pin_list.end());
+                        }
+
+                        for (const auto& gate_pin : pin_list)
+                        {
+                            const auto net = (gate_pin->get_direction() == PinDirection::output) ? g->get_fan_out_net(gate_pin) : g->get_fan_in_net(gate_pin);
+                            if (net == nullptr)
+                            {
+                                continue;
+                            }
+
+                            if (net->is_gnd_net() || net->is_vcc_net())
+                            {
+                                continue;
+                            }
+
+                            const auto module_pin = m->get_pin_by_net(net);
+
+                            module_pins.push_back(module_pin);
+                        }
+                    }
+
+                    m->create_pin_group(module_pg_name, module_pins);
+                    u32 idx_counter = 0;
+                    for (const auto& mp : module_pins)
+                    {
+                        m->set_pin_name(mp, module_pg_name + "_" + std::to_string(idx_counter));
+                        idx_counter++;
+                    }
+                }
+
+                all_modules.push_back(m);
+            }
+        }
+
+        return OK(all_modules);
+    }
+
 }    // namespace hal