diff options
Diffstat (limited to 'kernel/satgen.cc')
| -rw-r--r-- | kernel/satgen.cc | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/kernel/satgen.cc b/kernel/satgen.cc index 214826f5a..9c40ec66d 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -252,6 +252,106 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } + if (cell->type == ID($bmux)) + { + std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep); + std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep); + std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep); + std::vector<int> undef_a, undef_s, undef_y; + + if (model_undef) + { + undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep); + undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep); + undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep); + } + + if (GetSize(s) == 0) { + ez->vec_set(a, y); + if (model_undef) + ez->vec_set(undef_a, undef_y); + } else { + for (int i = GetSize(s)-1; i >= 0; i--) + { + std::vector<int> out = (i == 0) ? y : ez->vec_var(a.size() / 2); + std::vector<int> yy = model_undef ? ez->vec_var(out.size()) : out; + + std::vector<int> a0(a.begin(), a.begin() + a.size() / 2); + std::vector<int> a1(a.begin() + a.size() / 2, a.end()); + ez->assume(ez->vec_eq(ez->vec_ite(s.at(i), a1, a0), yy)); + + if (model_undef) + { + std::vector<int> undef_out = (i == 0) ? undef_y : ez->vec_var(a.size() / 2); + std::vector<int> undef_a0(undef_a.begin(), undef_a.begin() + a.size() / 2); + std::vector<int> undef_a1(undef_a.begin() + a.size() / 2, undef_a.end()); + std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a0, a1)); + std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a0, undef_a1)); + std::vector<int> yX = ez->vec_ite(undef_s.at(i), undef_ab, ez->vec_ite(s.at(i), undef_a1, undef_a0)); + ez->assume(ez->vec_eq(yX, undef_out)); + undefGating(out, yy, undef_out); + + undef_a = undef_out; + } + + a = out; + } + } + return true; + } + + if (cell->type == ID($demux)) + { + std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep); + std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep); + std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep); + std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y; + std::vector<int> undef_a, undef_s, undef_y; + + if (model_undef) + { + undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep); + undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep); + undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep); + } + + if (GetSize(s) == 0) { + ez->vec_set(a, y); + if (model_undef) + ez->vec_set(undef_a, undef_y); + } else { + for (int i = 0; i < (1 << GetSize(s)); i++) + { + std::vector<int> ss; + for (int j = 0; j < GetSize(s); j++) { + if (i & 1 << j) + ss.push_back(s[j]); + else + ss.push_back(ez->NOT(s[j])); + } + int sss = ez->expression(ezSAT::OpAnd, ss); + + for (int j = 0; j < GetSize(a); j++) { + ez->SET(ez->AND(sss, a[j]), yy.at(i * GetSize(a) + j)); + } + + if (model_undef) + { + int s0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(ss), ez->vec_not(undef_s))); + int us = ez->AND(ez->NOT(s0), ez->expression(ezSAT::OpOr, undef_s)); + for (int j = 0; j < GetSize(a); j++) { + int a0 = ez->AND(ez->NOT(a[j]), ez->NOT(undef_a[j])); + int yX = ez->AND(ez->OR(us, undef_a[j]), ez->NOT(ez->OR(s0, a0))); + ez->SET(yX, undef_y.at(i * GetSize(a) + j)); + } + } + } + if (model_undef) + undefGating(y, yy, undef_y); + } + return true; + } + if (cell->type == ID($pmux)) { std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep); |