Simplified $fa undef model

diff --git a/kernel/consteval.h b/kernel/consteval.h
index 6e507bd515df3a0212bddd22b22139deff47281e..2d29d3f7e3d2eec1eaad6d0860b1bef43bf9cbcd 100644 (file)
--- a/kernel/consteval.h
+++ b/kernel/consteval.h
@@ -214,6 +214,10 @@ struct ConstEval
                        RTLIL::Const t3 = const_and(sig_c.as_const(), t1, false, false, width);
                        RTLIL::Const val_x = const_or(t2, t3, false, false, width);
 
+                       for (int i = 0; i < SIZE(val_y); i++)
+                               if (val_y.bits[i] == RTLIL::Sx)
+                                       val_x.bits[i] = RTLIL::Sx;
+
                        set(sig_y, val_y);
                        set(sig_x, val_x);
                }

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 91f8ab40d27e21e3a58ce02b506adb6c933f3dda..692c6e7fb063ec1eadc668f7b5808584499889b3 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -991,20 +991,7 @@ struct SatGen
                                std::vector<int> undef_x = importUndefSigSpec(cell->getPort("\\X"), timestep);
 
                                ez->assume(ez->vec_eq(undef_y, ez->vec_or(ez->vec_or(undef_a, undef_b), undef_c)));
-
-                               std::vector<int> undef_t1 = ez->vec_or(undef_a, undef_b);
-
-                               std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
-                               std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
-                               std::vector<int> undef_t2 = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
-
-                               std::vector<int> c0 = ez->vec_and(ez->vec_not(c), ez->vec_not(undef_c));
-                               std::vector<int> t10 = ez->vec_and(ez->vec_not(t1), ez->vec_not(undef_t1));
-                               std::vector<int> undef_t3 = ez->vec_and(ez->vec_or(undef_c, undef_t1), ez->vec_not(ez->vec_or(c0, t10)));
-
-                               std::vector<int> t21 = ez->vec_and(t2, ez->vec_not(undef_t2));
-                               std::vector<int> t31 = ez->vec_and(t3, ez->vec_not(undef_t3));
-                               ez->assume(ez->vec_eq(undef_x, ez->vec_and(ez->vec_or(undef_t2, undef_t3), ez->vec_not(ez->vec_or(t21, t31)))));
+                               ez->assume(ez->vec_eq(undef_x, undef_y));
 
                                undefGating(y, yy, undef_y);
                                undefGating(x, xx, undef_x);

diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index da745b5e0bc30cae38e67e26db24ea3572ef9e38..dd12bd39f9b694a7978314962d7f0ab17d4d0ebc 100644 (file)
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -453,7 +453,7 @@ output [WIDTH-1:0] X, Y;
 wire [WIDTH-1:0] t1, t2, t3;
 
 assign t1 = A ^ B, t2 = A & B, t3 = C & t1;
-assign Y = t1 ^ C, X = t2 | t3;
+assign Y = t1 ^ C, X = (t2 | t3) ^ (Y ^ Y);
 
 endmodule