diff options
| -rw-r--r-- | kernel/consteval.h | 10 | ||||
| -rw-r--r-- | kernel/satgen.h | 43 |
2 files changed, 43 insertions, 10 deletions
diff --git a/kernel/consteval.h b/kernel/consteval.h index a424007e..10116ccf 100644 --- a/kernel/consteval.h +++ b/kernel/consteval.h @@ -110,6 +110,7 @@ struct ConstEval if (cell->type == "$mux" || cell->type == "$pmux" || cell->type == "$safe_pmux" || cell->type == "$_MUX_") { std::vector<RTLIL::SigSpec> y_candidates; + int count_maybe_set_s_bits = 0; int count_set_s_bits = 0; for (int i = 0; i < sig_s.width; i++) @@ -120,16 +121,17 @@ struct ConstEval if (s_bit == RTLIL::State::Sx || s_bit == RTLIL::State::S1) y_candidates.push_back(b_slice); + if (s_bit == RTLIL::State::S1 || s_bit == RTLIL::State::Sx) + count_maybe_set_s_bits++; + if (s_bit == RTLIL::State::S1) count_set_s_bits++; } - if (cell->type == "$safe_pmux" && count_set_s_bits > 1) { + if (cell->type == "$safe_pmux" && count_set_s_bits > 1) y_candidates.clear(); - count_set_s_bits = 0; - } - if (count_set_s_bits == 0) + if ((cell->type == "$safe_pmux" && count_maybe_set_s_bits > 1) || count_set_s_bits == 0) y_candidates.push_back(sig_a); std::vector<RTLIL::Const> y_values; diff --git a/kernel/satgen.h b/kernel/satgen.h index 208ae165..a668c73a 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -318,14 +318,45 @@ struct SatGen std::vector<int> undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); - tmp = a; - for (size_t i = 0; i < s.size(); i++) { + int maybe_one_hot = ez->FALSE; + int maybe_many_hot = ez->FALSE; + + int sure_one_hot = ez->FALSE; + int sure_many_hot = ez->FALSE; + + std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->FALSE); + std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->FALSE); + + for (size_t i = 0; i < s.size(); i++) + { + std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size()); std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size()); - tmp = ez->vec_ite(s.at(i), part_of_undef_b, tmp); + + int maybe_s = ez->OR(s.at(i), undef_s.at(i)); + int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i))); + + maybe_one_hot = ez->OR(maybe_one_hot, maybe_s); + maybe_many_hot = ez->OR(maybe_many_hot, ez->AND(maybe_one_hot, maybe_s)); + + sure_one_hot = ez->OR(sure_one_hot, sure_s); + sure_many_hot = ez->OR(sure_many_hot, ez->AND(sure_one_hot, sure_s)); + + bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b))), bits_set); + bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b))), bits_clr); + } + + int maybe_a = ez->NOT(maybe_one_hot); + + if (cell->type == "$safe_pmux") { + maybe_a = ez->OR(maybe_a, maybe_many_hot); + bits_set = ez->vec_ite(sure_many_hot, ez->vec_or(a, undef_a), bits_set); + bits_clr = ez->vec_ite(sure_many_hot, ez->vec_or(ez->vec_not(a), undef_a), bits_clr); } - tmp = ez->vec_ite(ez->onehot(s, true), tmp, cell->type == "$safe_pmux" ? a : std::vector<int>(tmp.size(), ez->TRUE)); - tmp = ez->vec_ite(ez->expression(ezSAT::OpOr, undef_s), std::vector<int>(tmp.size(), ez->TRUE), tmp); - ez->assume(ez->vec_eq(tmp, undef_y)); + + bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set); + bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr); + + ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y)); undefGating(y, yy, undef_y); } return true; |