Merge branch 'feature/word_level_structures' of github.com:emsec/hal …

…into feature/word_level_structures

plugins/bitwuzla_utils/src/subgraph_function_generator.cpp

@@ -154,7 +154,7 @@ namespace hal
             return get_subgraph_bitwuzla_function_internal(subgraph_gates, subgraph_output, net_cache, gate_cache);
         }
 
-        Result<std::vector<bitwuzla::Term>> get_subgraph_bitwuzla_functions(const std::vector<Gate*>& subgraph_gates, const std::vector<Net*> subgraph_outputs)
+        Result<std::vector<bitwuzla::Term>> get_subgraph_bitwuzla_functions(const std::vector<Gate*>& subgraph_gates, const std::vector<Net*>& subgraph_outputs)
         {
             std::map<u32, bitwuzla::Term> net_cache;
             std::map<std::pair<u32, const GatePin*>, BooleanFunction> gate_cache;

plugins/bitwuzla_utils/test/bitwuzla_utils.cpp

@@ -14,7 +14,7 @@ namespace hal
     protected:
         virtual void SetUp()
         {
-            NO_COUT_BLOCK;
+            // NO_COUT_BLOCK;
             test_utils::init_log_channels();
             test_utils::create_sandbox_directory();
         }
@@ -36,7 +36,7 @@ namespace hal
                 auto a    = BooleanFunction::Var("A", bits);
                 auto b    = BooleanFunction::Var("B", bits);
                 auto c    = BooleanFunction::Var("C", bits);
-                auto cond = BooleanFunction::Var("cond", 1);
+                auto cond = BooleanFunction::Eq(a.clone(), b.clone(), 1).get();
 
                 auto bf_not_res = BooleanFunction::Not(a.clone(), bits);
                 ASSERT_TRUE(bf_not_res.is_ok());
@@ -225,20 +225,19 @@ namespace hal
                 auto bft_ult = bft_ult_res.get();
                 EXPECT_EQ(bf_ult, bft_ult);
 
-                // auto bf_ite_res = BooleanFunction::Ite(cond.clone(), b.clone(), c.clone(), bits);
-                // ASSERT_TRUE(bf_ite_res.is_ok());
-                // auto bf_ite      = bf_ite_res.get();
-                // auto bff_ite_res = bitwuzla_utils::from_bf(bf_ite);
-                // ASSERT_TRUE(bff_ite_res.is_ok());    //
-                // auto bitwuzla_ite = bff_ite_res.get();
-                // auto bft_ite_res = bitwuzla_utils::to_bf(bitwuzla_ite);
-                // ASSERT_TRUE(bft_ite_res.is_ok());
-                // auto bft_ite = bft_ite_res.get();
-                // EXPECT_EQ(bf_ite, bft_ite);
+                auto bf_ite_res = BooleanFunction::Ite(cond.clone(), b.clone(), c.clone(), bits);
+                ASSERT_TRUE(bf_ite_res.is_ok());
+                auto bf_ite      = bf_ite_res.get();
+                auto bff_ite_res = bitwuzla_utils::from_bf(bf_ite);
+                ASSERT_TRUE(bff_ite_res.is_ok());    //
+                auto bitwuzla_ite = bff_ite_res.get();
+                auto bft_ite_res  = bitwuzla_utils::to_bf(bitwuzla_ite);
+                ASSERT_TRUE(bft_ite_res.is_ok());
+                auto bft_ite = bft_ite_res.get();
+                EXPECT_EQ(bf_ite, bft_ite);
             }
         }
         {
-            auto ctx = z3::context();
             auto a   = BooleanFunction::Var("A", 16);
             auto i0  = BooleanFunction::Index(3, 16);
             auto i1  = BooleanFunction::Index(6, 16);
@@ -255,7 +254,6 @@ namespace hal
             EXPECT_EQ(bf_slice, bft_slice);
         }
         {
-            // auto ctx      = z3::context();
             auto a        = BooleanFunction::Var("A", 5);
             auto ext_size = BooleanFunction::Index(16, 16);
 
@@ -282,7 +280,6 @@ namespace hal
             EXPECT_EQ(bf_sext, bft_sext);
         }
         {
-            // auto ctx      = z3::context();
             auto a        = BooleanFunction::Var("A", 16);
             auto num_bits = BooleanFunction::Index(5, 16);
 

plugins/netlist_preprocessing/python/python_bindings.cpp

@@ -238,7 +238,7 @@ namespace hal
                 Calls remove_unconnected_gates / remove_unconnected_nets until there are no further changes.
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
-                :returns: The total number of removed nets and gates on success, ``None`` otherwise.
+                :returns: The number of removed nets and gates on success, ``None`` otherwise.
                 :rtype: int or ``None``
             )");
 
@@ -261,12 +261,12 @@ namespace hal
             R"(
                 Apply manually implemented optimizations to the netlist centered around muxes.
                 Currently implemented optimizations include:
-                 - removing inverters incase there are inverter gates infront and behind every data input and output of the mux
+                 - removing inverters incase there are inverter gates in front and behind every data input and output of the mux
                  - optimizing and therefore unifying possible inverters preceding the select signals by resynthesizing
 
                 :param halp_py.Netlist nl: The netlist to operate on.
                 :param halp_py.GateLibrary mux_inv_gl: A gate library only containing mux and inverter gates used for resynthesis.
-                :returns: The difference in total gates caused by these optimizations.
+                :returns: The difference in the total number of gates caused by these optimizations.
                 :rtype: int or ``None``
             )");
 
@@ -289,7 +289,7 @@ namespace hal
                 Builds for all gate output nets the Boolean function and substitutes all variables connected to vcc/gnd nets with the respective boolean value.
                 If the function simplifies to a static boolean constant cut the connection to the nets destinations and directly connect it to vcc/gnd. 
 
-                :partam hal_py.Netlist nl: The netlist to operate on.
+                :param hal_py.Netlist nl: The netlist to operate on.
                 :returns: The number of rerouted nets on success, ``None`` otherwise.
                 :rtype: int or ``None``
             )");
@@ -426,25 +426,25 @@ namespace hal
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
                 :param hal_py.Gate g: The gate to resynthesize.
-                :param hal_py.GateLibrary target_lib: Gatelibrary containing the gates used for technology mapping.
-                :param path genlib_path: Path to file containg the target library in genlib format.
+                :param hal_py.GateLibrary target_lib: Gate library containing the gates used for technology mapping.
+                :param path genlib_path: Path to file containing the target library in genlib format.
                 :param bool delete_gate: Determines whether the original gate gets deleted by the function, defaults to true.
                 :returns: ``True`` on success, ``False`` otherwise.
                 :rtype: bool
             )");
 
         py_netlist_preprocessing.def_static(
             "resynthesize_gates",
-            [](Netlist* nl, const std::vector<Gate*>& gates, GateLibrary* target_lib) -> bool {
+            [](Netlist* nl, const std::vector<Gate*>& gates, GateLibrary* target_lib) -> std::optional<u32> {
                 auto res = NetlistPreprocessingPlugin::resynthesize_gates(nl, gates, target_lib);
                 if (res.is_ok())
                 {
-                    return true;
+                    return res.get();
                 }
                 else
                 {
                     log_error("python_context", "{}", res.get_error().get());
-                    return false;
+                    return std::nullopt;
                 }
             },
             py::arg("nl"),
@@ -456,9 +456,9 @@ namespace hal
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
                 :param hal_py.Gate g: The gates to resynthesize.
-                :param hal_py.GateLibrary target_lib: Gatelibrary containing the gates used for technology mapping.
-                :returns: ``True`` on success, ``False`` otherwise.
-                :rtype: bool
+                :param hal_py.GateLibrary target_lib: Gate library containing the gates used for technology mapping.
+                :returns: The number of resynthesized gates on success, ``None``otherwise.
+                :rtype: int or ``None``
             )");
 
         py_netlist_preprocessing.def_static(
@@ -484,7 +484,7 @@ namespace hal
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
                 :param list[hal_py.GateType] gate_types: The gate types specifying which gates should be resynthesized.
-                :param hal_py.GateLibrary target_lib: Gatelibrary containing the gates used for technology mapping.
+                :param hal_py.GateLibrary target_lib: Gate library containing the gates used for technology mapping.
                 :returns: The number of resynthesized gates on success, ``None`` otherwise.
                 :rtype: int or ``None``
             )");
@@ -512,7 +512,7 @@ namespace hal
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
                 :param list[hal_py.Gate] subgraph: The subgraph to be resynthesized.
-                :param hal_py.GateLibrary target_lib: Gatelibrary containing the gates used for technology mapping.
+                :param hal_py.GateLibrary target_lib: Gate library containing the gates used for technology mapping.
                 :returns: The number of resynthesized gates on success, ``None`` otherwise.
                 :rtype: int or ``None``
             )");
@@ -541,7 +541,7 @@ namespace hal
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
                 :param list[hal_py.GateType] gate_types: The gate types specifying which gates should be part of the subgraph.
-                :param hal_py.GateLibrary target_lib: Gatelibrary containing the gates used for technology mapping.
+                :param hal_py.GateLibrary target_lib: Gate library containing the gates used for technology mapping.
                 :returns: The number of resynthesized gates on success, ``None`` otherwise.
                 :rtype: int or ``None``
             )");
@@ -562,7 +562,7 @@ namespace hal
             },
             py::arg("nl"),
             R"(
-                Tries to reconstruct a name and index for each flip flop that was part of a multibit wire in the verilog code.
+                Tries to reconstruct a name and index for each flip flop that was part of a multi-bit wire in the verilog code.
                 This is NOT a general netlist reverse engineering algorithm and ONLY works on synthesized netlists with names annotated by the synthesizer.
                 This function mainly focuses netlists synthesized with yosys since yosys names the output wires of the flip flops but not the gate it self.
                 We try to reconstruct name and index for each flip flop based on the name of its output nets.
@@ -591,7 +591,7 @@ namespace hal
                 Tries to reconstruct top module pin groups via indexed pin names.
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
-                :returns: The number of reconstructed pingroups on success, ``None`` otherwise.
+                :returns: The number of reconstructed pin groups on success, ``None`` otherwise.
                 :rtype: int or ``None``
             )");
 
@@ -623,8 +623,8 @@ namespace hal
 
         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);
+            [](Netlist* nl, const std::map<std::string, std::map<std::string, std::vector<std::string>>>& concatenated_pin_groups) -> std::vector<Module*> {
+                auto res = NetlistPreprocessingPlugin::create_multi_bit_gate_modules(nl, concatenated_pin_groups);
                 if (res.is_ok())
                 {
                     return res.get();
@@ -636,16 +636,43 @@ namespace hal
                 }
             },
             py::arg("nl"),
-            py::arg("concatinated_pin_groups"),
+            py::arg("concatenated_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.
+                Create modules from large gates like RAMs and DSPs with the option to concat multiple gate pin groups to larger consecutive pin groups.
 
                 :param hal_py.Netlist nl: The netlist to operate on. 
-                :param  concatinated_pin_groups: 
+                :param  concatenated_pin_groups: 
                 :returns: ``True`` on success, ``False`` otherwise.
                 :rtype: bool
             )");
 
+        py_netlist_preprocessing.def_static(
+            "unify_ff_outputs",
+            [](Netlist* nl, const std::vector<Gate*>& ffs = {}) -> std::optional<u32> {
+                auto res = NetlistPreprocessingPlugin::unify_ff_outputs(nl, ffs);
+                if (res.is_ok())
+                {
+                    return res.get();
+                }
+                else
+                {
+                    log_error("python_context", "{}", res.get_error().get());
+                    return std::nullopt;
+                }
+            },
+            py::arg("nl"),
+            py::arg("ffs") = std::vector<Gate*>(),
+            R"(
+                Iterates all flip-flops of the netlist or specified by the user.
+                If a flip-flop has a ``state`` and a ``neg_state`` output, a new inverter gate is created and connected to the ``state`` output net as an additional destination.
+                Finally, the ``neg_state`` output net is disconnected from the ``neg_state`` pin and re-connected to the new inverter gate's output. 
+
+                :param hal_py.Netlist nl: The netlist to operate on. 
+                :param list[hal_py.Gate] ffs: The flip-flops to operate on. Defaults to an empty vector, in which case all flip-flops of the netlist are considered.
+                :returns: The number of rerouted ``neg_state`` outputs on success, ``None`` otherwise.
+                :rtype: int or ``None``
+            )");
+
 #ifndef PYBIND11_MODULE
         return m.ptr();
 #endif    // PYBIND11_MODULE

plugins/netlist_preprocessing/src/plugin_netlist_preprocessing.cpp

@@ -617,14 +617,14 @@ namespace hal
 #ifdef BITWUZLA_LIBRARY
         auto s_type = hal::SMT::SolverType::Bitwuzla;
         auto s_call = hal::SMT::SolverCall::Library;
-        config = config.with_solver(s_type).with_call(s_call);
+        config      = config.with_solver(s_type).with_call(s_call);
 #endif
         struct GateFingerprint
         {
             const GateType* type;
             std::map<GatePin*, Net*> ordered_fan_in = {};
-            std::set<Net*> unordered_fan_in  = {};
-            u8 trust_table_hw                = 0;
+            std::set<Net*> unordered_fan_in         = {};
+            u8 trust_table_hw                       = 0;
 
             bool operator<(const GateFingerprint& other) const
             {
@@ -861,7 +861,7 @@ namespace hal
 #ifdef BITWUZLA_LIBRARY
         auto s_type = hal::SMT::SolverType::Bitwuzla;
         auto s_call = hal::SMT::SolverCall::Library;
-        config = config.with_solver(s_type).with_call(s_call);
+        config      = config.with_solver(s_type).with_call(s_call);
 #endif
 
         u32 num_gates = 0;
@@ -1874,10 +1874,10 @@ namespace hal
     }
 
     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)
+                                                                                           const std::map<std::string, std::map<std::string, std::vector<std::string>>>& concatenated_pin_groups)
     {
         std::vector<Module*> all_modules;
-        for (const auto& [gt_name, pin_groups] : concatinated_pin_groups)
+        for (const auto& [gt_name, pin_groups] : concatenated_pin_groups)
         {
             const auto& gt = nl->get_gate_library()->get_gate_type_by_name(gt_name);
             if (gt == nullptr)
@@ -1894,7 +1894,7 @@ namespace hal
                     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);
+                        const auto& gate_pg = g->get_type()->get_pin_group_by_name(gate_pg_name);
 
                         if (gate_pg == nullptr)
                         {
@@ -1942,4 +1942,66 @@ namespace hal
         return OK(all_modules);
     }
 
+    Result<u32> NetlistPreprocessingPlugin::unify_ff_outputs(Netlist* nl, const std::vector<Gate*>& ffs)
+    {
+        if (nl == nullptr)
+        {
+            return ERR("netlist is a nullptr");
+        }
+
+        const auto* gl       = nl->get_gate_library();
+        const auto inv_types = gl->get_gate_types([](const GateType* gt) {
+            return gt->get_properties() == std::set<GateTypeProperty>({GateTypeProperty::c_inverter}) && gt->get_input_pins().size() == 1 && gt->get_output_pins().size() == 1;
+        });
+        if (inv_types.empty())
+        {
+            return ERR("gate library " + gl->get_name() + " of netlist does not contain an inverter gate");
+        }
+        auto* inv_gt     = inv_types.begin()->second;
+        auto inv_in_pin  = inv_gt->get_input_pins().front();
+        auto inv_out_pin = inv_gt->get_output_pins().front();
+
+        u32 ctr = 0;
+
+        const std::vector<Gate*>& gates = ffs.empty() ? nl->get_gates() : ffs;
+
+        for (const auto* ff : gates)
+        {
+            if (!ff->get_type()->has_property(GateTypeProperty::ff))
+            {
+                continue;
+            }
+
+            auto out_eps = ff->get_fan_out_endpoints();
+
+            Endpoint* q_out  = nullptr;
+            Endpoint* qn_out = nullptr;
+
+            for (auto* ep : out_eps)
+            {
+                auto ep_type = ep->get_pin()->get_type();
+                if (ep_type == PinType::state)
+                {
+                    q_out = ep;
+                }
+                else if (ep_type == PinType::neg_state)
+                {
+                    qn_out = ep;
+                }
+            }
+
+            if (q_out != nullptr && qn_out != nullptr)
+            {
+                auto* inv = nl->create_gate(inv_gt, ff->get_name() + "_QN_INV");
+                q_out->get_net()->add_destination(inv, inv_in_pin);
+                auto* qn_net = qn_out->get_net();
+                qn_net->remove_source(qn_out);
+                qn_net->add_source(inv, inv_out_pin);
+                ctr++;
+            }
+        }
+
+        return OK(ctr);
+    }
+
 }    // namespace hal

plugins/z3_utils/src/z3_utils.cpp

@@ -100,7 +100,7 @@ namespace hal
                     case BooleanFunction::NodeType::Ult:
                         return {true, z3::ult(p[0], p[1])};
                     case BooleanFunction::NodeType::Ite:
-                        return {true, z3::ite(p[0] == context.bv_val(1, 1), p[1], p[2])};
+                        return {true, z3::ite(p[0], p[1], p[2])};
                     default:
                         log_error("netlist", "Not implemented reached for nodetype {} in z3 conversion", node.type);
                         return {false, z3::expr(context)};