current state

plugins/bitwuzla_utils/src/symbolic_execution.cpp

@@ -601,6 +601,8 @@ namespace hal
                         return true;
                     }
                 }
+
+                return false;
             }
 
             bool is_commutative(const bitwuzla::Term& x)

plugins/netlist_preprocessing/src/resynthesis.cpp

@@ -147,15 +147,31 @@ namespace hal
                         const auto& net_connections = global_io_mapping.at(src_n);
                         new_net                     = net_connections.front();
 
-                        // if a single global output leads to multiple nets in the dst netlist, that means that the nets are functionally equivalent and we can connect/merge them.
-                        for (u32 i = 1; i < net_connections.size(); i++)
+                        if (net_connections.size() != 1)
                         {
-                            const auto& res = NetlistModificationDecorator(*dst_nl).connect_nets(new_net, net_connections.at(i));
-                            if (res.is_error())
+                            log_warning(
+                                "resynthesis", "Found multiple io connections for net {} with ID {}, this might lead to missing nets in the destination netlist", src_n->get_name(), src_n->get_id());
+                            for (const auto& net : net_connections)
                             {
-                                return ERR("unable to replace subgraph with netlist: failed to connect/merge all the net connections of net " + src_n->get_name() + " with ID "
-                                           + std::to_string(src_n->get_id()));
+                                std::cout << net->get_id() << " - " << net->get_name() << std::endl;
                             }
+
+                            // if a single global output of the src netlist leads to multiple nets in the dst netlist, that means that the nets are functionally equivalent and we can connect/merge them.
+                            // however this can lead to nets disappearing from the dst netlist which might be unexpected behavior.
+
+                            for (u32 i = 1; i < net_connections.size(); i++)
+                            {
+                                const auto& res = NetlistModificationDecorator(*dst_nl).connect_nets(new_net, net_connections.at(i));
+                                if (res.is_error())
+                                {
+                                    return ERR("unable to replace subgraph with netlist: failed to connect/merge all the net connections of net " + src_n->get_name() + " with ID "
+                                               + std::to_string(src_n->get_id()));
+                                }
+                            }
+                        }
+                        else
+                        {
+                            new_net = net_connections.front();
                         }
                     }
                     else
@@ -190,7 +206,7 @@ namespace hal
                     const auto org_src_name     = src_ep->get_gate()->get_name();
                     const auto org_src_pin_name = src_ep->get_pin()->get_name();
                     auto new_src_g              = gate_name_to_gate.at(org_src_name);
-                    if (!new_net->add_source(new_src_g, org_src_pin_name))
+                    if (new_net->add_source(new_src_g, org_src_pin_name) == nullptr)
                     {
                         return ERR("unable to replace subgraph with netlist: failed to add gate " + new_src_g->get_name() + " with ID " + std::to_string(new_src_g->get_id()) + " at pin "
                                    + org_src_pin_name + " as new source to net " + new_net->get_name() + " with ID " + std::to_string(new_net->get_id()));

plugins/z3_utils/src/simplification.cpp

@@ -2307,6 +2307,9 @@ namespace hal
 
         Result<z3::expr> simplify_local(const z3::expr& e, const bool check)
         {
+            const u32 max_loop_iterations = 128;
+            u32 iteration                 = 0;
+
             z3::expr res      = e;
             z3::expr prev_res = res;
 
@@ -2324,6 +2327,17 @@ namespace hal
                 }
                 const auto [it, _] = cache.insert({e.id(), simplify_res.get()});
                 res                = it->second;
+
+                iteration++;
+                if (iteration > max_loop_iterations)
+                {
+                    std::cout << "PREV: " << std::endl;
+                    std::cout << prev_res << std::endl;
+                    std::cout << "CURR: " << std::endl;
+                    std::cout << res << std::endl;
+
+                    return ERR("Triggered max iteration counter during simplificaton!");
+                }
             } while (!z3::eq(prev_res, res));
 
             if (check && !check_correctness(e, res))

plugins/z3_utils/src/z3_utils.cpp

@@ -204,6 +204,7 @@ namespace hal
                     }
                     else if (e.is_const())
                     {
+                        // std::cout << e << std::endl;
                         const std::string name = e.decl().name().str();
                         return OK(BooleanFunction::Var(name, size));
                     }

src/netlist/boolean_function/symbolic_execution.cpp

@@ -132,6 +132,20 @@ namespace hal
              */
             BooleanFunction Add(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
             {
+                if (p0.size() <= 64 && p1.size() <= 64)
+                {
+                    const auto a_res = BooleanFunction::to_u64(p0);
+                    const auto b_res = BooleanFunction::to_u64(p1);
+
+                    if (a_res.is_ok() && b_res.is_ok())
+                    {
+                        const auto res = (a_res.get() + b_res.get()) & 0xffffffff;
+                        return BooleanFunction::Const(res, p0.size());
+                    }
+
+                    return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
+                }
+
                 if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
                     || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
                 {
@@ -159,6 +173,20 @@ namespace hal
              */
             BooleanFunction Sub(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
             {
+                if (p0.size() <= 64 && p1.size() <= 64)
+                {
+                    const auto a_res = BooleanFunction::to_u64(p0);
+                    const auto b_res = BooleanFunction::to_u64(p1);
+
+                    if (a_res.is_ok() && b_res.is_ok())
+                    {
+                        const auto res = (a_res.get() - b_res.get()) & 0xffffffff;
+                        return BooleanFunction::Const(res, p0.size());
+                    }
+
+                    return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
+                }
+
                 if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
                     || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
                 {