riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Fixed SAT and ConstEval undef handling for $pmux and $safe_pmux

This commit is contained in:
Clifford Wolf 2014-01-03 17:30:50 +01:00
parent 8a8d444648
commit 7354a1718e
2 changed files with 43 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
kernel/consteval.h
View File

@ -110,6 +110,7 @@ struct ConstEval
if (cell->type == "$mux" || cell->type == "$pmux" || cell->type == "$safe_pmux" || cell->type == "$_MUX_") if (cell->type == "$mux" || cell->type == "$pmux" || cell->type == "$safe_pmux" || cell->type == "$_MUX_")
{ {
std::vector<RTLIL::SigSpec> y_candidates; std::vector<RTLIL::SigSpec> y_candidates;
int count_maybe_set_s_bits = 0;
int count_set_s_bits = 0; int count_set_s_bits = 0;
for (int i = 0; i < sig_s.width; i++) 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) if (s_bit == RTLIL::State::Sx || s_bit == RTLIL::State::S1)
y_candidates.push_back(b_slice); 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) if (s_bit == RTLIL::State::S1)
count_set_s_bits++; 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(); 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); y_candidates.push_back(sig_a);
std::vector<RTLIL::Const> y_values; std::vector<RTLIL::Const> y_values;

43
kernel/satgen.h
View File

@ -318,14 +318,45 @@ struct SatGen
std::vector<int> undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep); std::vector<int> undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
tmp = a; int maybe_one_hot = ez->FALSE;
for (size_t i = 0; i < s.size(); i++) { 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()); 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);
} }
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); int maybe_a = ez->NOT(maybe_one_hot);
ez->assume(ez->vec_eq(tmp, undef_y));
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);
}
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); undefGating(y, yy, undef_y);
} }
return true; return true;