Improvements and fixes in SAT code

diff --git a/kernel/satgen.h b/kernel/satgen.h
index b7bd87dd4b9a78fbafde742a7fd287a4f72dfbc0..5b3a4d041393cebed200c5f8e7dd694ddce50cc4 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -74,22 +74,22 @@ struct SatGen
                return vec;
        }
 
-       void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell)
+       void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0)
        {
                bool is_signed_a = false, is_signed_b = false;
                if (cell->parameters.count("\\A_SIGNED") > 0)
                        is_signed_a = cell->parameters["\\A_SIGNED"].as_bool();
                if (cell->parameters.count("\\B_SIGNED") > 0)
                        is_signed_b = cell->parameters["\\B_SIGNED"].as_bool();
-               while (vec_a.size() < vec_b.size())
+               while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
                        vec_a.push_back(is_signed_a && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
-               while (vec_b.size() < vec_a.size())
+               while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
                        vec_b.push_back(is_signed_b && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
        }
 
        void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell)
        {
-               extendSignalWidth(vec_a, vec_b, cell);
+               extendSignalWidth(vec_a, vec_b, cell, vec_y.size());
                while (vec_y.size() < vec_a.size())
                        vec_y.push_back(ez->literal());
        }
@@ -239,6 +239,23 @@ struct SatGen
                        return true;
                }
 
+               if (cell->type == "$mul") {
+                       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> tmp(a.size(), ez->FALSE);
+                       for (int i = 0; i < int(a.size()); i++)
+                       {
+                               std::vector<int> shifted_a(a.size(), ez->FALSE);
+                               for (int j = i; j < int(a.size()); j++)
+                                       shifted_a.at(j) = a.at(j-i);
+                               tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
+                       }
+                       ez->assume(ez->vec_eq(tmp, y));
+                       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")));
@@ -250,7 +267,7 @@ struct SatGen
                        return true;
                }
 
-               // Unsupported internal cell types: $mul $div $mod $pow
+               // Unsupported internal cell types: $div $mod $pow
                // .. and all sequential cells except $dff and $_DFF_[NP]_
                return false;
        }

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index a13f83183997c715f72ac32ce0ad2e140f4dcb90..e5f678820c7727b2a15721ee89ea09324db920d3 100644 (file)
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -41,6 +41,11 @@ static void split(std::vector<std::string> &tokens, const std::string &text, cha
        tokens.push_back(text.substr(start));
 }
 
+static int get_dummy_line_num()
+{
+       return 0;
+}
+
 static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
 {
        std::vector<std::string> tokens;
@@ -56,6 +61,7 @@ static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string
                        continue;
 
                if ('0' <= netname[0] && netname[0] <= '9') {
+                       AST::get_line_num = get_dummy_line_num;
                        AST::AstNode *ast = VERILOG_FRONTEND::const2ast(netname);
                        if (ast == NULL)
                                return false;
@@ -320,7 +326,7 @@ struct SatHelper
                                                        continue;
                                                if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
                                                        continue;
-                                               queued_signals.add(handled_signals.remove(p.second));
+                                               queued_signals.add(handled_signals.remove(sigmap(p.second)));
                                        }
                                }
                        }
@@ -712,6 +718,8 @@ struct SatPass : public Pass {
                        sathelper.ez.printDIMACS(stdout, true);
 #endif
 
+                       bool did_rerun = false;
+
                rerun_solver:
                        log("\nSolving problem with %d variables and %d clauses..\n",
                                        sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
@@ -733,16 +741,18 @@ struct SatPass : public Pass {
                                }
 
                                if (loopcount != 0) {
-                                       loopcount--;
+                                       loopcount--, did_rerun = true;
                                        sathelper.invalidate_model();
                                        goto rerun_solver;
                                }
                        }
                        else
                        {
-                               if (prove.size() == 0) {
+                               if (did_rerun)
+                                       log("SAT solving finished - no more models found.\n");
+                               else if (prove.size() == 0)
                                        log("SAT solving finished - no model found.\n");
-                               } else {
+                               else {
                                        log("SAT proof finished - no model found: SUCCESS!\n");
                                        print_qed();
                                }