diff --git a/kernel/satgen.cc b/kernel/satgen.cc index 2a1fd1711..3c21a8f99 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -375,29 +375,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) std::vector undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep); std::vector undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep); - int maybe_a = ez->CONST_TRUE; + int all_undef = ez->CONST_FALSE; + int found_active = ez->CONST_FALSE; - std::vector bits_set = std::vector(undef_y.size(), ez->CONST_FALSE); - std::vector bits_clr = std::vector(undef_y.size(), ez->CONST_FALSE); + std::vector undef_tmp = undef_a; for (size_t i = 0; i < s.size(); i++) { - std::vector part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size()); std::vector part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size()); - 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_a = ez->AND(maybe_a, ez->NOT(sure_s)); - - bits_set = ez->vec_ite(maybe_s, 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(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr); + undef_tmp = ez->vec_ite(s.at(i), part_of_undef_b, undef_tmp); + all_undef = ez->OR(all_undef, undef_s.at(i)); + all_undef = ez->OR(all_undef, ez->AND(s.at(i), found_active)); + found_active = ez->OR(found_active, s.at(i)); } - 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); + undef_tmp = ez->vec_or(undef_tmp, std::vector(a.size(), all_undef)); - ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y)); + ez->assume(ez->vec_eq(undef_tmp, undef_y)); undefGating(y, yy, undef_y); } return true; diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index e64697efb..b5e437d90 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1331,10 +1331,17 @@ always @* begin Y = A; found_active_sel_bit = 0; for (i = 0; i < S_WIDTH; i = i+1) - if (S[i]) begin - Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i); - found_active_sel_bit = 1; - end + case (S[i]) + 1'b1: begin + Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i); + found_active_sel_bit = 1; + end + 1'b0: ; + 1'bx: begin + Y = 'bx; + found_active_sel_bit = 'bx; + end + endcase end endmodule