Fix undef propagation bug in $pmux SAT model

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 690f8e337471d129b3d02836029ab218d09602a6..25a22fd8a2ca0dd4f5f3c7aa60faec91459081b8 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -507,11 +507,7 @@ struct SatGen
                                std::vector<int> undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep);
                                std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
 
-                               int maybe_one_hot = ez->CONST_FALSE;
-                               int maybe_many_hot = ez->CONST_FALSE;
-
-                               int sure_one_hot = ez->CONST_FALSE;
-                               int sure_many_hot = ez->CONST_FALSE;
+                               int maybe_a = ez->CONST_TRUE;
 
                                std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
                                std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
@@ -524,18 +520,12 @@ struct SatGen
                                        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_one_hot = ez->OR(maybe_one_hot, maybe_s);
-                                       maybe_many_hot = ez->OR(maybe_many_hot, ez->AND(maybe_one_hot, maybe_s));
-
-                                       sure_one_hot = ez->OR(sure_one_hot, sure_s);
-                                       sure_many_hot = ez->OR(sure_many_hot, ez->AND(sure_one_hot, sure_s));
+                                       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(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(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b))), bits_clr);
+                                       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);
                                }
 
-                               int maybe_a = ez->NOT(maybe_one_hot);
-
                                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);