diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-01-02 19:58:59 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-01-02 19:58:59 +0100 |
| commit | 1f80557adeede4d6fb90bab76e9a8acc2450136c (patch) | |
| tree | 9f0a158b0e7e151f21648131c988cff46d683e21 /kernel | |
| parent | 0759c97748dc159bacc4a25fd83b6fddfe618bc6 (diff) | |
| download | yosys-1f80557adeede4d6fb90bab76e9a8acc2450136c.tar.gz yosys-1f80557adeede4d6fb90bab76e9a8acc2450136c.tar.bz2 yosys-1f80557adeede4d6fb90bab76e9a8acc2450136c.zip | |
Added SAT undef model for $pmux and $safe_pmux
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/satgen.h | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index 510240f59..208ae1658 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -299,6 +299,9 @@ struct SatGen std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep); std::vector<int> s = importDefSigSpec(cell->connections.at("\\S"), timestep); std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep); + + std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y; + std::vector<int> tmp = a; 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()); @@ -306,12 +309,24 @@ struct SatGen } if (cell->type == "$safe_pmux") tmp = ez->vec_ite(ez->onehot(s, true), tmp, a); - ez->assume(ez->vec_eq(tmp, y)); + ez->assume(ez->vec_eq(tmp, yy)); - if (model_undef) { - log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type)); + if (model_undef) + { + std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep); + std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep); + std::vector<int> undef_s = importUndefSigSpec(cell->connections.at("\\S"), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); - ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_y))); + + tmp = a; + for (size_t i = 0; i < s.size(); i++) { + 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); + } + 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)); + undefGating(y, yy, undef_y); } return true; } |