Added SAT model for $alu cells

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 5d1c11c9ebc88b89e499709fa8e07e85a278233f..beb037686c7e6da6050f9b77d8ad059ef768c441 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -183,9 +183,9 @@ struct SatGen
        bool importCell(RTLIL::Cell *cell, int timestep = -1)
        {
                bool arith_undef_handled = false;
-               bool is_arith_compare = cell->type == "$lt" || cell->type == "$le" || cell->type == "$ge" || cell->type == "$gt";
+               bool is_arith_compare = cell->type.in("$lt", "$le", "$ge", "$gt");
 
-               if (model_undef && (cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || cell->type == "$mod" || is_arith_compare))
+               if (model_undef && (cell->type.in("$add", "$sub", "$mul", "$div", "$mod") || is_arith_compare))
                {
                        std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
                        std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
@@ -891,6 +891,73 @@ struct SatGen
                        return true;
                }
 
+               if (cell->type == "$alu")
+               {
+                       std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
+                       std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
+                       std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
+                       std::vector<int> x = importDefSigSpec(cell->getPort("\\X"), timestep);
+                       std::vector<int> ci = importDefSigSpec(cell->getPort("\\CI"), timestep);
+                       std::vector<int> bi = importDefSigSpec(cell->getPort("\\BI"), timestep);
+                       std::vector<int> co = importDefSigSpec(cell->getPort("\\CO"), timestep);
+
+                       extendSignalWidth(a, b, y, cell);
+                       extendSignalWidth(a, b, x, cell);
+                       extendSignalWidth(a, b, co, cell);
+
+                       std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
+                       std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
+                       std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
+
+                       log_assert(SIZE(y) == SIZE(x));
+                       log_assert(SIZE(y) == SIZE(co));
+                       log_assert(SIZE(ci) == 1);
+                       log_assert(SIZE(bi) == 1);
+
+                       for (int i = 0; i < SIZE(y); i++)
+                       {
+                               int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
+                               ez->SET(def_x.at(i), ez->XOR(s1, s2));
+                               ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
+                               ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
+                       }
+
+                       if (model_undef)
+                       {
+                               std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
+                               std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
+                               std::vector<int> undef_ci = importUndefSigSpec(cell->getPort("\\CI"), timestep);
+                               std::vector<int> undef_bi = importUndefSigSpec(cell->getPort("\\BI"), timestep);
+
+                               std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
+                               std::vector<int> undef_x = importUndefSigSpec(cell->getPort("\\X"), timestep);
+                               std::vector<int> undef_co = importUndefSigSpec(cell->getPort("\\CO"), timestep);
+
+                               extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
+                               extendSignalWidth(undef_a, undef_b, undef_x, cell, true);
+                               extendSignalWidth(undef_a, undef_b, undef_co, cell, true);
+
+                               std::vector<int> all_inputs_undef;
+                               all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
+                               all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
+                               all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
+                               all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
+                               int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
+
+                               for (int i = 0; i < SIZE(undef_y); i++) {
+                                       ez->SET(undef_y.at(i), undef_any);
+                                       ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
+                                       ez->SET(undef_co.at(i), undef_any);
+                               }
+
+                               undefGating(y, def_y, undef_y);
+                               undefGating(x, def_x, undef_x);
+                               undefGating(co, def_co, undef_co);
+                       }
+                       log_ping();
+                       return true;
+               }
+
                if (cell->type == "$slice")
                {
                        RTLIL::SigSpec a = cell->getPort("\\A");