diff --git a/plugins/bitwuzla_utils/src/symbolic_execution.cpp b/plugins/bitwuzla_utils/src/symbolic_execution.cpp index aad10afe8b2..78f7e8b3f98 100644 --- a/plugins/bitwuzla_utils/src/symbolic_execution.cpp +++ b/plugins/bitwuzla_utils/src/symbolic_execution.cpp @@ -601,6 +601,8 @@ namespace hal return true; } } + + return false; } bool is_commutative(const bitwuzla::Term& x) diff --git a/plugins/netlist_preprocessing/src/resynthesis.cpp b/plugins/netlist_preprocessing/src/resynthesis.cpp index 17b8207c165..2ce8c4e1842 100644 --- a/plugins/netlist_preprocessing/src/resynthesis.cpp +++ b/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())); diff --git a/plugins/z3_utils/src/simplification.cpp b/plugins/z3_utils/src/simplification.cpp index 8db0e7a2fbd..54ac2f2a5a1 100644 --- a/plugins/z3_utils/src/simplification.cpp +++ b/plugins/z3_utils/src/simplification.cpp @@ -2307,6 +2307,9 @@ namespace hal Result 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)) diff --git a/plugins/z3_utils/src/z3_utils.cpp b/plugins/z3_utils/src/z3_utils.cpp index fba4aa07f35..e6184b67900 100644 --- a/plugins/z3_utils/src/z3_utils.cpp +++ b/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)); } diff --git a/src/netlist/boolean_function/symbolic_execution.cpp b/src/netlist/boolean_function/symbolic_execution.cpp index 1be338d6192..702b366d44a 100644 --- a/src/netlist/boolean_function/symbolic_execution.cpp +++ b/src/netlist/boolean_function/symbolic_execution.cpp @@ -132,6 +132,20 @@ namespace hal */ BooleanFunction Add(const std::vector& p0, const std::vector& 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(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& p0, const std::vector& 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(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; })) {