passes/sat/sat.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 // [[CITE]] Temporal Induction by Incremental SAT Solving
  21 // Niklas Een and Niklas Sörensson (2003)
  22 // http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161
  23
  24 #include "kernel/register.h"
  25 #include "kernel/celltypes.h"
  26 #include "kernel/consteval.h"
  27 #include "kernel/sigtools.h"
  28 #include "kernel/log.h"
  29 #include "kernel/satgen.h"
  30 #include <stdlib.h>
  31 #include <stdio.h>
  32 #include <algorithm>
  33
  34 namespace {
  35
  36 struct SatHelper
  37 {
  38         RTLIL::Design *design;
  39         RTLIL::Module *module;
  40
  41         ezDefaultSAT ez;
  42         SigMap sigmap;
  43         CellTypes ct;
  44         SatGen satgen;
  45
  46         // additional constraints
  47         std::vector<std::pair<std::string, std::string>> sets, prove;
  48         std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
  49         std::map<int, std::vector<std::string>> unsets_at;
  50
  51         // undef constraints
  52         bool enable_undef;
  53         std::vector<std::string> sets_def, sets_undef, sets_all_undef;
  54         std::map<int, std::vector<std::string>> sets_def_at, sets_undef_at, sets_all_undef_at;
  55
  56         // model variables
  57         std::vector<std::string> shows;
  58         SigPool show_signal_pool;
  59         SigSet<RTLIL::Cell*> show_drivers;
  60         int max_timestep, timeout;
  61         bool gotTimeout;
  62
  63         SatHelper(RTLIL::Design *design, RTLIL::Module *module) :
  64                 design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap)
  65         {
  66                 enable_undef = false;
  67                 max_timestep = -1;
  68                 timeout = 0;
  69                 gotTimeout = false;
  70         }
  71
  72         void setup(int timestep = -1)
  73         {
  74                 if (timestep > 0)
  75                         log ("\nSetting up time step %d:\n", timestep);
  76                 else
  77                         log ("\nSetting up SAT problem:\n");
  78
  79                 if (timestep > max_timestep)
  80                         max_timestep = timestep;
  81
  82                 RTLIL::SigSpec big_lhs, big_rhs;
  83
  84                 for (auto &s : sets)
  85                 {
  86                         RTLIL::SigSpec lhs, rhs;
  87
  88                         if (!RTLIL::SigSpec::parse(lhs, module, s.first))
  89                                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
  90                         if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
  91                                 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
  92                         show_signal_pool.add(sigmap(lhs));
  93                         show_signal_pool.add(sigmap(rhs));
  94
  95                         if (lhs.width != rhs.width)
  96                                 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
  97                                         s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
  98
  99                         log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
 100                         big_lhs.remove2(lhs, &big_rhs);
 101                         big_lhs.append(lhs);
 102                         big_rhs.append(rhs);
 103                 }
 104
 105                 for (auto &s : sets_at[timestep])
 106                 {
 107                         RTLIL::SigSpec lhs, rhs;
 108
 109                         if (!RTLIL::SigSpec::parse(lhs, module, s.first))
 110                                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
 111                         if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
 112                                 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
 113                         show_signal_pool.add(sigmap(lhs));
 114                         show_signal_pool.add(sigmap(rhs));
 115
 116                         if (lhs.width != rhs.width)
 117                                 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
 118                                         s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
 119
 120                         log("Import set-constraint for timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
 121                         big_lhs.remove2(lhs, &big_rhs);
 122                         big_lhs.append(lhs);
 123                         big_rhs.append(rhs);
 124                 }
 125
 126                 for (auto &s : unsets_at[timestep])
 127                 {
 128                         RTLIL::SigSpec lhs;
 129
 130                         if (!RTLIL::SigSpec::parse(lhs, module, s))
 131                                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
 132                         show_signal_pool.add(sigmap(lhs));
 133
 134                         log("Import unset-constraint for timestep: %s\n", log_signal(lhs));
 135                         big_lhs.remove2(lhs, &big_rhs);
 136                 }
 137
 138                 log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
 139
 140                 std::vector<int> lhs_vec = satgen.importSigSpec(big_lhs, timestep);
 141                 std::vector<int> rhs_vec = satgen.importSigSpec(big_rhs, timestep);
 142                 ez.assume(ez.vec_eq(lhs_vec, rhs_vec));
 143
 144                 int import_cell_counter = 0;
 145                 for (auto &c : module->cells)
 146                         if (design->selected(module, c.second)) {
 147                                 // log("Import cell: %s\n", RTLIL::id2cstr(c.first));
 148                                 if (satgen.importCell(c.second, timestep)) {
 149                                         for (auto &p : c.second->connections)
 150                                                 if (ct.cell_output(c.second->type, p.first))
 151                                                         show_drivers.insert(sigmap(p.second), c.second);
 152                                         import_cell_counter++;
 153                                 } else
 154                                         log("Warning: failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
 155                 }
 156                 log("Imported %d cells to SAT database.\n", import_cell_counter);
 157         }
 158
 159         int setup_proof(int timestep = -1)
 160         {
 161                 assert(prove.size() > 0);
 162
 163                 RTLIL::SigSpec big_lhs, big_rhs;
 164
 165                 for (auto &s : prove)
 166                 {
 167                         RTLIL::SigSpec lhs, rhs;
 168
 169                         if (!RTLIL::SigSpec::parse(lhs, module, s.first))
 170                                 log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
 171                         if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
 172                                 log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
 173                         show_signal_pool.add(sigmap(lhs));
 174                         show_signal_pool.add(sigmap(rhs));
 175
 176                         if (lhs.width != rhs.width)
 177                                 log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
 178                                         s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
 179
 180                         log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
 181                         big_lhs.remove2(lhs, &big_rhs);
 182                         big_lhs.append(lhs);
 183                         big_rhs.append(rhs);
 184                 }
 185
 186                 log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
 187
 188                 std::vector<int> lhs_vec = satgen.importSigSpec(big_lhs, timestep);
 189                 std::vector<int> rhs_vec = satgen.importSigSpec(big_rhs, timestep);
 190                 return ez.vec_eq(lhs_vec, rhs_vec);
 191         }
 192
 193         void force_unique_state(int timestep_from, int timestep_to)
 194         {
 195                 RTLIL::SigSpec state_signals = satgen.initial_state.export_all();
 196                 for (int i = timestep_from; i < timestep_to; i++)
 197                         ez.assume(ez.vec_ne(satgen.importSigSpec(state_signals, i), satgen.importSigSpec(state_signals, timestep_to)));
 198         }
 199
 200         bool solve(const std::vector<int> &assumptions)
 201         {
 202                 // undef is work in progress
 203                 log_assert(enable_undef == false);
 204
 205                 log_assert(gotTimeout == false);
 206                 ez.setSolverTimeout(timeout);
 207                 bool success = ez.solve(modelExpressions, modelValues, assumptions);
 208                 if (ez.getSolverTimoutStatus())
 209                         gotTimeout = true;
 210                 return success;
 211         }
 212
 213         bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
 214         {
 215                 // undef is work in progress
 216                 log_assert(enable_undef == false);
 217
 218                 log_assert(gotTimeout == false);
 219                 ez.setSolverTimeout(timeout);
 220                 bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
 221                 if (ez.getSolverTimoutStatus())
 222                         gotTimeout = true;
 223                 return success;
 224         }
 225
 226         struct ModelBlockInfo {
 227                 int timestep, offset, width;
 228                 std::string description;
 229                 bool operator < (const ModelBlockInfo &other) const {
 230                         if (timestep != other.timestep)
 231                                 return timestep < other.timestep;
 232                         if (description != other.description)
 233                                 return description < other.description;
 234                         if (offset != other.offset)
 235                                 return offset < other.offset;
 236                         if (width != other.width)
 237                                 return width < other.width;
 238                         return false;
 239                 }
 240         };
 241
 242         std::vector<int> modelExpressions;
 243         std::vector<bool> modelValues;
 244         std::set<ModelBlockInfo> modelInfo;
 245
 246         void generate_model()
 247         {
 248                 RTLIL::SigSpec modelSig;
 249                 modelExpressions.clear();
 250                 modelInfo.clear();
 251
 252                 // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals
 253
 254                 if (shows.size() == 0)
 255                 {
 256                         SigPool queued_signals, handled_signals, final_signals;
 257                         queued_signals = show_signal_pool;
 258                         while (queued_signals.size() > 0) {
 259                                 RTLIL::SigSpec sig = queued_signals.export_one();
 260                                 queued_signals.del(sig);
 261                                 handled_signals.add(sig);
 262                                 std::set<RTLIL::Cell*> drivers = show_drivers.find(sig);
 263                                 if (drivers.size() == 0) {
 264                                         final_signals.add(sig);
 265                                 } else {
 266                                         for (auto &d : drivers)
 267                                         for (auto &p : d->connections) {
 268                                                 if (d->type == "$dff" && p.first == "\\CLK")
 269                                                         continue;
 270                                                 if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
 271                                                         continue;
 272                                                 queued_signals.add(handled_signals.remove(sigmap(p.second)));
 273                                         }
 274                                 }
 275                         }
 276                         modelSig = final_signals.export_all();
 277
 278                         // additionally add all set and prove signals directly
 279                         // (it improves user confidence if we write the constraints back ;-)
 280                         modelSig.append(show_signal_pool.export_all());
 281                 }
 282                 else
 283                 {
 284                         for (auto &s : shows) {
 285                                 RTLIL::SigSpec sig;
 286                                 if (!RTLIL::SigSpec::parse(sig, module, s))
 287                                         log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str());
 288                                 log("Import show expression: %s\n", log_signal(sig));
 289                                 modelSig.append(sig);
 290                         }
 291                 }
 292
 293                 modelSig.sort_and_unify();
 294                 // log("Model signals: %s\n", log_signal(modelSig));
 295
 296                 for (auto &c : modelSig.chunks)
 297                         if (c.wire != NULL) {
 298                                 ModelBlockInfo info;
 299                                 RTLIL::SigSpec chunksig = c;
 300                                 info.width = chunksig.width;
 301                                 info.description = log_signal(chunksig);
 302
 303                                 for (int timestep = -1; timestep <= max_timestep; timestep++) {
 304                                         if ((timestep == -1 && max_timestep > 0) || timestep == 0)
 305                                                 continue;
 306                                         std::vector<int> vec = satgen.importSigSpec(chunksig, timestep);
 307                                         info.timestep = timestep;
 308                                         info.offset = modelExpressions.size();
 309                                         modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
 310                                         modelInfo.insert(info);
 311                                 }
 312                         }
 313
 314                 // Add zero step signals as collected by satgen
 315
 316                 modelSig = satgen.initial_state.export_all();
 317                 for (auto &c : modelSig.chunks)
 318                         if (c.wire != NULL) {
 319                                 ModelBlockInfo info;
 320                                 RTLIL::SigSpec chunksig = c;
 321                                 info.timestep = 0;
 322                                 info.offset = modelExpressions.size();
 323                                 info.width = chunksig.width;
 324                                 info.description = log_signal(chunksig);
 325                                 std::vector<int> vec = satgen.importSigSpec(chunksig, 1);
 326                                 modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
 327                                 modelInfo.insert(info);
 328                         }
 329         }
 330
 331         void print_model()
 332         {
 333                 int maxModelName = 10;
 334                 int maxModelWidth = 10;
 335
 336                 for (auto &info : modelInfo) {
 337                         maxModelName = std::max(maxModelName, int(info.description.size()));
 338                         maxModelWidth = std::max(maxModelWidth, info.width);
 339                 }
 340
 341                 log("\n");
 342
 343                 int last_timestep = -2;
 344                 for (auto &info : modelInfo)
 345                 {
 346                         RTLIL::Const value;
 347                         for (int i = 0; i < info.width; i++) {
 348                                 value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
 349                                 if (modelValues.size() == 2*modelExpressions.size() && modelValues.at(modelExpressions.size()+info.offset+i))
 350                                         value.bits.back() = RTLIL::State::Sx;
 351                         }
 352
 353                         if (info.timestep != last_timestep) {
 354                                 const char *hline = "---------------------------------------------------------------------------------------------------"
 355                                                     "---------------------------------------------------------------------------------------------------"
 356                                                     "---------------------------------------------------------------------------------------------------";
 357                                 if (last_timestep == -2) {
 358                                         log(max_timestep > 0 ? "  Time " : "  ");
 359                                         log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");
 360                                 }
 361                                 log(max_timestep > 0 ? "  ---- " : "  ");
 362                                 log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10,
 363                                                 hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline);
 364                                 last_timestep = info.timestep;
 365                         }
 366
 367                         if (max_timestep > 0) {
 368                                 if (info.timestep > 0)
 369                                         log("  %4d ", info.timestep);
 370                                 else
 371                                         log("  init ");
 372                         } else
 373                                 log("  ");
 374
 375                         if (info.width <= 32)
 376                                 log("%-*s %10d %10x %*s\n", maxModelName+10, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+5, value.as_string().c_str());
 377                         else
 378                                 log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str());
 379                 }
 380
 381                 if (last_timestep == -2)
 382                         log("  no model variables selected for display.\n");
 383         }
 384
 385         void invalidate_model()
 386         {
 387                 std::vector<int> clause;
 388                 for (size_t i = 0; i < modelExpressions.size(); i++)
 389                         clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i));
 390                 ez.assume(ez.expression(ezSAT::OpOr, clause));
 391         }
 392 };
 393
 394 } /* namespace */
 395
 396 static void print_proof_failed()
 397 {
 398         log("\n");
 399         log("   ______                   ___       ___       _ _            _ _ \n");
 400         log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
 401         log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
 402         log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
 403         log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
 404         log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
 405         log("\n");
 406 }
 407
 408 static void print_timeout()
 409 {
 410         log("\n");
 411         log("        _____  _  _      _____ ____  _     _____\n");
 412         log("       /__ __\\/ \\/ \\__/|/  __//  _ \\/ \\ /\\/__ __\\\n");
 413         log("         / \\  | || |\\/|||  \\  | / \\|| | ||  / \\\n");
 414         log("         | |  | || |  |||  /_ | \\_/|| \\_/|  | |\n");
 415         log("         \\_/  \\_/\\_/  \\|\\____\\\\____/\\____/  \\_/\n");
 416         log("\n");
 417 }
 418
 419 static void print_qed()
 420 {
 421         log("\n");
 422         log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
 423         log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
 424         log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
 425         log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
 426         log("                | $$  | $$    | $$__/       | $$  | $$   \n");
 427         log("                | $$/$$ $$    | $$          | $$  | $$   \n");
 428         log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
 429         log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
 430         log("                       \\__/                              \n");
 431         log("\n");
 432 }
 433
 434 struct SatPass : public Pass {
 435         SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
 436         virtual void help()
 437         {
 438                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 439                 log("\n");
 440                 log("    sat [options] [selection]\n");
 441                 log("\n");
 442                 log("This command solves a SAT problem defined over the currently selected circuit\n");
 443                 log("and additional constraints passed as parameters.\n");
 444                 log("\n");
 445                 log("    -all\n");
 446                 log("        show all solutions to the problem (this can grow exponentially, use\n");
 447                 log("        -max <N> instead to get <N> solutions)\n");
 448                 log("\n");
 449                 log("    -max <N>\n");
 450                 log("        like -all, but limit number of solutions to <N>\n");
 451                 log("\n");
 452                 log("    -enable_undef\n");
 453                 log("        enable modeling of undef value (aka 'x-bits')\n");
 454                 log("        this option is implied by -set-def, -set-undef et. cetera\n");
 455                 log("\n");
 456                 log("    -set <signal> <value>\n");
 457                 log("        set the specified signal to the specified value.\n");
 458                 log("\n");
 459         #if 0
 460                 log("    -set-def <signal>\n");
 461                 log("        add a constraint that all bits of the given signal must be defined\n");
 462                 log("\n");
 463                 log("    -set-undef <signal>\n");
 464                 log("        add a constraint that at least one bit of the given signal is undefined\n");
 465                 log("\n");
 466                 log("    -set-all-undef <signal>\n");
 467                 log("        add a constraint that all bits of the given signal are undefined\n");
 468                 log("\n");
 469         #endif
 470                 log("    -show <signal>\n");
 471                 log("        show the model for the specified signal. if no -show option is\n");
 472                 log("        passed then a set of signals to be shown is automatically selected.\n");
 473                 log("\n");
 474                 log("    -ignore_div_by_zero\n");
 475                 log("        ignore all solutions that involve a division by zero\n");
 476                 log("\n");
 477                 log("The following options can be used to set up a sequential problem:\n");
 478                 log("\n");
 479                 log("    -seq <N>\n");
 480                 log("        set up a sequential problem with <N> time steps. The steps will\n");
 481                 log("        be numbered from 1 to N.\n");
 482                 log("\n");
 483                 log("    -set-at <N> <signal> <value>\n");
 484                 log("    -unset-at <N> <signal>\n");
 485                 log("        set or unset the specified signal to the specified value in the\n");
 486                 log("        given timestep. this has priority over a -set for the same signal.\n");
 487                 log("\n");
 488         #if 0
 489                 log("    -set-def <N> <signal>\n");
 490                 log("    -set-undef <N> <signal>\n");
 491                 log("    -set-all-undef <N> <signal>\n");
 492                 log("        add undef contraints in the given timestep.\n");
 493                 log("\n");
 494         #endif
 495                 log("The following additional options can be used to set up a proof. If also -seq\n");
 496                 log("is passed, a temporal induction proof is performed.\n");
 497                 log("\n");
 498                 log("    -prove <signal> <value>\n");
 499                 log("        Attempt to proof that <signal> is always <value>. In a temporal\n");
 500                 log("        induction proof it is proven that the condition holds forever after\n");
 501                 log("        the number of time steps passed using -seq.\n");
 502                 log("\n");
 503                 log("    -maxsteps <N>\n");
 504                 log("        Set a maximum length for the induction.\n");
 505                 log("\n");
 506                 log("    -timeout <N>\n");
 507                 log("        Maximum number of seconds a single SAT instance may take.\n");
 508                 log("\n");
 509                 log("    -verify\n");
 510                 log("        Return an error and stop the synthesis script if the proof fails.\n");
 511                 log("\n");
 512                 log("    -verify-no-timeout\n");
 513                 log("        Like -verify but do not return an error for timeouts.\n");
 514                 log("\n");
 515         }
 516         virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 517         {
 518                 std::vector<std::pair<std::string, std::string>> sets, prove;
 519                 std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 520                 std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_undef_at, sets_all_undef_at;
 521                 std::vector<std::string> shows, sets_def, sets_undef, sets_all_undef;
 522                 int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
 523                 bool verify = false, fail_on_timeout = false, enable_undef = false, ignore_div_by_zero = false;
 524
 525                 log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 526
 527                 size_t argidx;
 528                 for (argidx = 1; argidx < args.size(); argidx++) {
 529                         if (args[argidx] == "-all") {
 530                                 loopcount = -1;
 531                                 continue;
 532                         }
 533                         if (args[argidx] == "-verify") {
 534                                 fail_on_timeout = true;
 535                                 verify = true;
 536                                 continue;
 537                         }
 538                         if (args[argidx] == "-verify-no-timeout") {
 539                                 verify = true;
 540                                 continue;
 541                         }
 542                         if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
 543                                 timeout = atoi(args[++argidx].c_str());
 544                                 continue;
 545                         }
 546                         if (args[argidx] == "-max" && argidx+1 < args.size()) {
 547                                 loopcount = atoi(args[++argidx].c_str());
 548                                 continue;
 549                         }
 550                         if (args[argidx] == "-maxsteps" && argidx+1 < args.size()) {
 551                                 maxsteps = atoi(args[++argidx].c_str());
 552                                 continue;
 553                         }
 554                         if (args[argidx] == "-ignore_div_by_zero") {
 555                                 ignore_div_by_zero = true;
 556                                 continue;
 557                         }
 558                         if (args[argidx] == "-enable_undef") {
 559                                 enable_undef = true;
 560                                 continue;
 561                         }
 562                         if (args[argidx] == "-set" && argidx+2 < args.size()) {
 563                                 std::string lhs = args[++argidx];
 564                                 std::string rhs = args[++argidx];
 565                                 sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
 566                                 continue;
 567                         }
 568                         if (args[argidx] == "-set-def" && argidx+2 < args.size()) {
 569                                 sets_def.push_back(args[++argidx]);
 570                                 enable_undef = true;
 571                                 continue;
 572                         }
 573                         if (args[argidx] == "-set-undef" && argidx+2 < args.size()) {
 574                                 sets_undef.push_back(args[++argidx]);
 575                                 enable_undef = true;
 576                                 continue;
 577                         }
 578                         if (args[argidx] == "-set-all-undef" && argidx+2 < args.size()) {
 579                                 sets_all_undef.push_back(args[++argidx]);
 580                                 enable_undef = true;
 581                                 continue;
 582                         }
 583                         if (args[argidx] == "-prove" && argidx+2 < args.size()) {
 584                                 std::string lhs = args[++argidx];
 585                                 std::string rhs = args[++argidx];
 586                                 prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
 587                                 continue;
 588                         }
 589                         if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 590                                 seq_len = atoi(args[++argidx].c_str());
 591                                 continue;
 592                         }
 593                         if (args[argidx] == "-set-at" && argidx+3 < args.size()) {
 594                                 int timestep = atoi(args[++argidx].c_str());
 595                                 std::string lhs = args[++argidx];
 596                                 std::string rhs = args[++argidx];
 597                                 sets_at[timestep].push_back(std::pair<std::string, std::string>(lhs, rhs));
 598                                 continue;
 599                         }
 600                         if (args[argidx] == "-unset-at" && argidx+2 < args.size()) {
 601                                 int timestep = atoi(args[++argidx].c_str());
 602                                 unsets_at[timestep].push_back(args[++argidx]);
 603                                 continue;
 604                         }
 605                         if (args[argidx] == "-set-def-at" && argidx+2 < args.size()) {
 606                                 int timestep = atoi(args[++argidx].c_str());
 607                                 sets_def_at[timestep].push_back(args[++argidx]);
 608                                 enable_undef = true;
 609                                 continue;
 610                         }
 611                         if (args[argidx] == "-set-undef-at" && argidx+2 < args.size()) {
 612                                 int timestep = atoi(args[++argidx].c_str());
 613                                 sets_undef_at[timestep].push_back(args[++argidx]);
 614                                 enable_undef = true;
 615                                 continue;
 616                         }
 617                         if (args[argidx] == "-set-all-undef-at" && argidx+2 < args.size()) {
 618                                 int timestep = atoi(args[++argidx].c_str());
 619                                 sets_all_undef_at[timestep].push_back(args[++argidx]);
 620                                 enable_undef = true;
 621                                 continue;
 622                         }
 623                         if (args[argidx] == "-show" && argidx+1 < args.size()) {
 624                                 shows.push_back(args[++argidx]);
 625                                 continue;
 626                         }
 627                         break;
 628                 }
 629                 extra_args(args, argidx, design);
 630
 631                 RTLIL::Module *module = NULL;
 632                 for (auto &mod_it : design->modules)
 633                         if (design->selected(mod_it.second)) {
 634                                 if (module)
 635                                         log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n",
 636                                                         RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
 637                                 module = mod_it.second;
 638                         }
 639                 if (module == NULL)
 640                         log_cmd_error("Can't perform SAT on an empty selection!\n");
 641
 642                 if (prove.size() == 0 && verify)
 643                         log_cmd_error("Got -verify but nothing to prove!\n");
 644
 645                 if (prove.size() > 0 && seq_len > 0)
 646                 {
 647                         if (loopcount > 0)
 648                                 log_cmd_error("The options -max and -all are not supported for temporal induction proofs!\n");
 649
 650                         SatHelper basecase(design, module);
 651                         SatHelper inductstep(design, module);
 652
 653                         basecase.sets = sets;
 654                         basecase.prove = prove;
 655                         basecase.sets_at = sets_at;
 656                         basecase.unsets_at = unsets_at;
 657                         basecase.shows = shows;
 658                         basecase.timeout = timeout;
 659                         basecase.enable_undef = enable_undef;
 660                         basecase.sets_def = sets_def;
 661                         basecase.sets_undef = sets_undef;
 662                         basecase.sets_all_undef = sets_all_undef;
 663                         basecase.sets_def_at = sets_def_at;
 664                         basecase.sets_undef_at = sets_undef_at;
 665                         basecase.sets_all_undef_at = sets_all_undef_at;
 666                         basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
 667
 668                         for (int timestep = 1; timestep <= seq_len; timestep++)
 669                                 basecase.setup(timestep);
 670
 671                         inductstep.sets = sets;
 672                         inductstep.prove = prove;
 673                         inductstep.shows = shows;
 674                         inductstep.timeout = timeout;
 675                         inductstep.enable_undef = enable_undef;
 676                         inductstep.sets_def = sets_def;
 677                         inductstep.sets_undef = sets_undef;
 678                         inductstep.sets_all_undef = sets_all_undef;
 679                         inductstep.sets_def_at = sets_def_at;
 680                         inductstep.sets_undef_at = sets_undef_at;
 681                         inductstep.sets_all_undef_at = sets_all_undef_at;
 682                         inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
 683
 684                         inductstep.setup(1);
 685                         inductstep.ez.assume(inductstep.setup_proof(1));
 686
 687                         for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
 688                         {
 689                                 log("\n** Trying induction with length %d **\n", inductlen);
 690
 691                                 // phase 1: proving base case
 692
 693                                 basecase.setup(seq_len + inductlen);
 694                                 int property = basecase.setup_proof(seq_len + inductlen);
 695                                 basecase.generate_model();
 696
 697                                 if (inductlen > 1)
 698                                         basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
 699
 700                                 log("\n[base case] Solving problem with %d variables and %d clauses..\n",
 701                                                 basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses());
 702
 703                                 if (basecase.solve(basecase.ez.NOT(property))) {
 704                                         log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
 705                                         print_proof_failed();
 706                                         basecase.print_model();
 707                                         goto tip_failed;
 708                                 }
 709
 710                                 if (basecase.gotTimeout)
 711                                         goto timeout;
 712
 713                                 log("Base case for induction length %d proven.\n", inductlen);
 714                                 basecase.ez.assume(property);
 715
 716                                 // phase 2: proving induction step
 717
 718                                 inductstep.setup(inductlen + 1);
 719                                 property = inductstep.setup_proof(inductlen + 1);
 720                                 inductstep.generate_model();
 721
 722                                 if (inductlen > 1)
 723                                         inductstep.force_unique_state(1, inductlen + 1);
 724
 725                                 log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
 726                                                 inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
 727
 728                                 if (!inductstep.solve(inductstep.ez.NOT(property))) {
 729                                         if (inductstep.gotTimeout)
 730                                                 goto timeout;
 731                                         log("Induction step proven: SUCCESS!\n");
 732                                         print_qed();
 733                                         goto tip_success;
 734                                 }
 735
 736                                 log("Induction step failed. Incrementing induction length.\n");
 737                                 inductstep.ez.assume(property);
 738
 739                                 inductstep.print_model();
 740                         }
 741
 742                         log("\nReached maximum number of time steps -> proof failed.\n");
 743                         print_proof_failed();
 744
 745                 tip_failed:
 746                         if (verify) {
 747                                 log("\n");
 748                                 log_error("Called with -verify and proof did fail!\n");
 749                         }
 750
 751                 tip_success:;
 752                 }
 753                 else
 754                 {
 755                         if (maxsteps > 0)
 756                                 log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
 757
 758                         SatHelper sathelper(design, module);
 759                         sathelper.sets = sets;
 760                         sathelper.prove = prove;
 761                         sathelper.sets_at = sets_at;
 762                         sathelper.unsets_at = unsets_at;
 763                         sathelper.shows = shows;
 764                         sathelper.timeout = timeout;
 765                         sathelper.enable_undef = enable_undef;
 766                         sathelper.sets_def = sets_def;
 767                         sathelper.sets_undef = sets_undef;
 768                         sathelper.sets_all_undef = sets_all_undef;
 769                         sathelper.sets_def_at = sets_def_at;
 770                         sathelper.sets_undef_at = sets_undef_at;
 771                         sathelper.sets_all_undef_at = sets_all_undef_at;
 772                         sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
 773
 774                         if (seq_len == 0) {
 775                                 sathelper.setup();
 776                                 if (sathelper.prove.size() > 0)
 777                                         sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
 778                         } else {
 779                                 for (int timestep = 1; timestep <= seq_len; timestep++)
 780                                         sathelper.setup(timestep);
 781                         }
 782                         sathelper.generate_model();
 783
 784 #if 0
 785                         // print CNF for debugging
 786                         sathelper.ez.printDIMACS(stdout, true);
 787 #endif
 788
 789                         bool did_rerun = false;
 790
 791                 rerun_solver:
 792                         log("\nSolving problem with %d variables and %d clauses..\n",
 793                                         sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
 794
 795                         if (sathelper.solve())
 796                         {
 797                                 if (prove.size() == 0) {
 798                                         log("SAT solving finished - model found:\n");
 799                                 } else {
 800                                         log("SAT proof finished - model found: FAIL!\n");
 801                                         print_proof_failed();
 802                                 }
 803
 804                                 sathelper.print_model();
 805
 806                                 if (loopcount != 0) {
 807                                         loopcount--, did_rerun = true;
 808                                         sathelper.invalidate_model();
 809                                         goto rerun_solver;
 810                                 }
 811
 812                                 if (verify) {
 813                                         log("\n");
 814                                         log_error("Called with -verify and proof did fail!\n");
 815                                 }
 816                         }
 817                         else
 818                         {
 819                                 if (sathelper.gotTimeout)
 820                                         goto timeout;
 821                                 if (did_rerun)
 822                                         log("SAT solving finished - no more models found.\n");
 823                                 else if (prove.size() == 0)
 824                                         log("SAT solving finished - no model found.\n");
 825                                 else {
 826                                         log("SAT proof finished - no model found: SUCCESS!\n");
 827                                         print_qed();
 828                                 }
 829                         }
 830
 831                         if (verify && did_rerun) {
 832                                 log("\n");
 833                                 log_error("Called with -verify and proof did fail!\n");
 834                         }
 835                 }
 836
 837                 if (0) {
 838         timeout:
 839                         log("Interrupted SAT solver: TIMEOUT!\n");
 840                         print_timeout();
 841                         if (fail_on_timeout)
 842                                 log_error("Called with -verify and proof did time out!\n");
 843                 }
 844         }
 845 } SatPass;
 846