Added SAT support for $div and $mod cells

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 26e3fd7ec66a4dc2e29b9c0f0effc0e6f94e334a..b2f8b15b72a411ff5f923ebb51fae0a5d8a90f73 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -267,6 +267,52 @@ struct SatGen
                        return true;
                }
 
+               if (cell->type == "$div" || cell->type == "$mod")
+               {
+                       std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
+                       std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
+                       std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
+                       extendSignalWidth(a, b, y, cell);
+
+                       std::vector<int> a_u, b_u;
+                       if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
+                               a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
+                               b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
+                       } else {
+                               a_u = a;
+                               b_u = b;
+                       }
+
+                       std::vector<int> chain_buf = a_u;
+                       std::vector<int> y_u(a_u.size(), ez->FALSE);
+                       for (int i = int(a.size())-1; i >= 0; i--)
+                       {
+                               chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->FALSE);
+
+                               std::vector<int> b_shl(i, ez->FALSE);
+                               b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
+                               b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->FALSE);
+
+                               y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
+                               chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
+
+                               chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
+                       }
+
+                       if (cell->type == "$div") {
+                               if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
+                                       ez->assume(ez->vec_eq(y, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
+                               else
+                                       ez->assume(ez->vec_eq(y, y_u));
+                       } else {
+                               if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
+                                       ez->assume(ez->vec_eq(y, ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf)));
+                               else
+                                       ez->assume(ez->vec_eq(y, chain_buf));
+                       }
+                       return true;
+               }
+
                if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) {
                        if (timestep == 1) {
                                initial_state.add((*sigmap)(cell->connections.at("\\Q")));

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 00918f62f7a022f7f1f0701f6aa589e1ac3532b6..4258fb6fe6bcd72cd998e87b8e4e521e5f1a6514 100644 (file)
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -852,6 +852,12 @@ std::vector<int> ezSAT::vec_sub(const std::vector<int> &vec1, const std::vector<
        return vec;
 }
 
+std::vector<int> ezSAT::vec_neg(const std::vector<int> &vec)
+{
+       std::vector<int> zero(vec.size(), FALSE);
+       return vec_sub(zero, vec);
+}
+
 void ezSAT::vec_cmp(const std::vector<int> &vec1, const std::vector<int> &vec2, int &carry, int &overflow, int &sign, int &zero)
 {
        assert(vec1.size() == vec2.size());

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 2d0307d5124e7964e0ae15bb0e9849b88fc35021..4a6a72785008886af6903e488f09ed4ee6f335d3 100644 (file)
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -223,6 +223,7 @@ public:
        std::vector<int> vec_count(const std::vector<int> &vec, int bits, bool clip = true);
        std::vector<int> vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2);
        std::vector<int> vec_sub(const std::vector<int> &vec1, const std::vector<int> &vec2);
+       std::vector<int> vec_neg(const std::vector<int> &vec);
 
        void vec_cmp(const std::vector<int> &vec1, const std::vector<int> &vec2, int &carry, int &overflow, int &sign, int &zero);
 
@@ -305,6 +306,8 @@ struct ezSATvec
        ezSATvec(ezSAT &sat, const std::vector<int> &vec) : sat(sat), vec(vec) { }
 
        ezSATvec operator ~() { return ezSATvec(sat, sat.vec_not(vec)); }
+       ezSATvec operator -() { return ezSATvec(sat, sat.vec_neg(vec)); }
+
        ezSATvec operator &(const ezSATvec &other) { return ezSATvec(sat, sat.vec_and(vec, other.vec)); }
        ezSATvec operator |(const ezSATvec &other) { return ezSATvec(sat, sat.vec_or(vec, other.vec)); }
        ezSATvec operator ^(const ezSATvec &other) { return ezSATvec(sat, sat.vec_xor(vec, other.vec)); }