diff --git a/kernel/satgen.cc b/kernel/satgen.cc index a6003bd06..60c9c8538 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -430,7 +430,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } - if (cell->type.in(ID($pos), ID($buf), ID($neg), ID($connect))) + if (cell->type.in(ID($pos), ID($buf), ID($neg))) { std::vector a = importDefSigSpec(cell->getPort(ID::A), timestep); std::vector y = importDefSigSpec(cell->getPort(ID::Y), timestep); @@ -438,7 +438,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) std::vector yy = model_undef ? ez->vec_var(y.size()) : y; - if (cell->type.in(ID($pos), ID($buf), ID($connect))) { + if (cell->type.in(ID($pos), ID($buf))) { ez->assume(ez->vec_eq(a, yy)); } else { std::vector zero(a.size(), ez->CONST_FALSE); @@ -451,7 +451,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) std::vector undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep); extendSignalWidthUnary(undef_a, undef_y, cell); - if (cell->type.in(ID($pos), ID($buf), ID($connect))) { + if (cell->type.in(ID($pos), ID($buf))) { ez->assume(ez->vec_eq(undef_a, undef_y)); } else { int undef_any_a = ez->expression(ezSAT::OpOr, undef_a); @@ -464,6 +464,26 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } + if (cell->type.in(ID($connect))) + { + std::vector a = importDefSigSpec(cell->getPort(ID::A), timestep); + std::vector b = importDefSigSpec(cell->getPort(ID::B), timestep); + extendSignalWidthUnary(a, b, cell); + + std::vector bb = model_undef ? ez->vec_var(b.size()) : b; + ez->assume(ez->vec_eq(a, bb)); + + if (model_undef) + { + std::vector undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep); + std::vector undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep); + extendSignalWidthUnary(undef_a, undef_b, cell); + ez->assume(ez->vec_eq(undef_a, undef_b)); + undefGating(b, bb, undef_b); + } + return true; + } + if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool), ID($logic_not))) { std::vector a = importDefSigSpec(cell->getPort(ID::A), timestep);