diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-07-21 12:03:41 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-07-21 12:03:41 +0200 |
| commit | c54d1f2ad1a781363f9c35e4f7266f4560a6aba8 (patch) | |
| tree | e48a916d74c8e42ef933c9f6bf0abd90ee130b9d /kernel | |
| parent | 54b0f2e659ac0c34c69b0c251c72b2a90fe8e6b6 (diff) | |
| download | yosys-c54d1f2ad1a781363f9c35e4f7266f4560a6aba8.tar.gz yosys-c54d1f2ad1a781363f9c35e4f7266f4560a6aba8.tar.bz2 yosys-c54d1f2ad1a781363f9c35e4f7266f4560a6aba8.zip | |
Bugfix in satgen for cells with wider in- than outputs.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/satgen.h | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index 81d029295..281d2b26f 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -166,7 +166,15 @@ struct SatGen void undefGating(std::vector<int> &vec_y, std::vector<int> &vec_yy, std::vector<int> &vec_undef) { assert(model_undef); - ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy)))); + assert(vec_y.size() == vec_yy.size()); + if (vec_y.size() > vec_undef.size()) { + std::vector<int> trunc_y(vec_y.begin(), vec_y.begin() + vec_undef.size()); + std::vector<int> trunc_yy(vec_yy.begin(), vec_yy.begin() + vec_undef.size()); + ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(trunc_y, trunc_yy)))); + } else { + assert(vec_y.size() == vec_undef.size()); + ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy)))); + } } bool importCell(RTLIL::Cell *cell, int timestep = -1) |