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         // model variables
  52         std::vector<std::string> shows;
  53         SigPool show_signal_pool;
  54         SigSet<RTLIL::Cell*> show_drivers;
  55         int max_timestep, timeout;
  56         bool gotTimeout;
  57
  58         SatHelper(RTLIL::Design *design, RTLIL::Module *module) :
  59                 design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap)
  60         {
  61                 max_timestep = -1;
  62                 timeout = 0;
  63                 gotTimeout = false;
  64         }
  65
  66         void setup(int timestep = -1)
  67         {
  68                 if (timestep > 0)
  69                         log ("\nSetting up time step %d:\n", timestep);
  70                 else
  71                         log ("\nSetting up SAT problem:\n");
  72
  73                 if (timestep > max_timestep)
  74                         max_timestep = timestep;
  75
  76                 RTLIL::SigSpec big_lhs, big_rhs;
  77
  78                 for (auto &s : sets)
  79                 {
  80                         RTLIL::SigSpec lhs, rhs;
  81
  82                         if (!RTLIL::SigSpec::parse(lhs, module, s.first))
  83                                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
  84                         if (!RTLIL::SigSpec::parse(rhs, module, s.second))
  85                                 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
  86                         show_signal_pool.add(sigmap(lhs));
  87                         show_signal_pool.add(sigmap(rhs));
  88
  89                         if (lhs.width != rhs.width)
  90                                 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
  91                                         s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
  92
  93                         log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
  94                         big_lhs.remove2(lhs, &big_rhs);
  95                         big_lhs.append(lhs);
  96                         big_rhs.append(rhs);
  97                 }
  98
  99                 for (auto &s : sets_at[timestep])
 100                 {
 101                         RTLIL::SigSpec lhs, rhs;
 102
 103                         if (!RTLIL::SigSpec::parse(lhs, module, s.first))
 104                                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
 105                         if (!RTLIL::SigSpec::parse(rhs, module, s.second))
 106                                 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
 107                         show_signal_pool.add(sigmap(lhs));
 108                         show_signal_pool.add(sigmap(rhs));
 109
 110                         if (lhs.width != rhs.width)
 111                                 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
 112                                         s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
 113
 114                         log("Import set-constraint for timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
 115                         big_lhs.remove2(lhs, &big_rhs);
 116                         big_lhs.append(lhs);
 117                         big_rhs.append(rhs);
 118                 }
 119
 120                 for (auto &s : unsets_at[timestep])
 121                 {
 122                         RTLIL::SigSpec lhs;
 123
 124                         if (!RTLIL::SigSpec::parse(lhs, module, s))
 125                                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
 126                         show_signal_pool.add(sigmap(lhs));
 127
 128                         log("Import unset-constraint for timestep: %s\n", log_signal(lhs));
 129                         big_lhs.remove2(lhs, &big_rhs);
 130                 }
 131
 132                 log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
 133
 134                 std::vector<int> lhs_vec = satgen.importSigSpec(big_lhs, timestep);
 135                 std::vector<int> rhs_vec = satgen.importSigSpec(big_rhs, timestep);
 136                 ez.assume(ez.vec_eq(lhs_vec, rhs_vec));
 137
 138                 int import_cell_counter = 0;
 139                 for (auto &c : module->cells)
 140                         if (design->selected(module, c.second)) {
 141                                 // log("Import cell: %s\n", RTLIL::id2cstr(c.first));
 142                                 if (satgen.importCell(c.second, timestep)) {
 143                                         for (auto &p : c.second->connections)
 144                                                 if (ct.cell_output(c.second->type, p.first))
 145                                                         show_drivers.insert(sigmap(p.second), c.second);
 146                                         import_cell_counter++;
 147                                 } else
 148                                         log("Warning: failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
 149                 }
 150                 log("Imported %d cells to SAT database.\n", import_cell_counter);
 151         }
 152
 153         int setup_proof(int timestep = -1)
 154         {
 155                 assert(prove.size() > 0);
 156
 157                 RTLIL::SigSpec big_lhs, big_rhs;
 158
 159                 for (auto &s : prove)
 160                 {
 161                         RTLIL::SigSpec lhs, rhs;
 162
 163                         if (!RTLIL::SigSpec::parse(lhs, module, s.first))
 164                                 log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
 165                         if (!RTLIL::SigSpec::parse(rhs, module, s.second))
 166                                 log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
 167                         show_signal_pool.add(sigmap(lhs));
 168                         show_signal_pool.add(sigmap(rhs));
 169
 170                         if (lhs.width != rhs.width)
 171                                 log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
 172                                         s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
 173
 174                         log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
 175                         big_lhs.remove2(lhs, &big_rhs);
 176                         big_lhs.append(lhs);
 177                         big_rhs.append(rhs);
 178                 }
 179
 180                 log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
 181
 182                 std::vector<int> lhs_vec = satgen.importSigSpec(big_lhs, timestep);
 183                 std::vector<int> rhs_vec = satgen.importSigSpec(big_rhs, timestep);
 184                 return ez.vec_eq(lhs_vec, rhs_vec);
 185         }
 186
 187         void force_unique_state(int timestep_from, int timestep_to)
 188         {
 189                 RTLIL::SigSpec state_signals = satgen.initial_state.export_all();
 190                 for (int i = timestep_from; i < timestep_to; i++)
 191                         ez.assume(ez.vec_ne(satgen.importSigSpec(state_signals, i), satgen.importSigSpec(state_signals, timestep_to)));
 192         }
 193
 194         bool solve(const std::vector<int> &assumptions)
 195         {
 196                 log_assert(gotTimeout == false);
 197                 ez.setSolverTimeout(timeout);
 198                 bool success = ez.solve(modelExpressions, modelValues, assumptions);
 199                 if (ez.getSolverTimoutStatus())
 200                         gotTimeout = true;
 201                 return success;
 202         }
 203
 204         bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
 205         {
 206                 log_assert(gotTimeout == false);
 207                 ez.setSolverTimeout(timeout);
 208                 bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
 209                 if (ez.getSolverTimoutStatus())
 210                         gotTimeout = true;
 211                 return success;
 212         }
 213
 214         struct ModelBlockInfo {
 215                 int timestep, offset, width;
 216                 std::string description;
 217                 bool operator < (const ModelBlockInfo &other) const {
 218                         if (timestep != other.timestep)
 219                                 return timestep < other.timestep;
 220                         if (description != other.description)
 221                                 return description < other.description;
 222                         if (offset != other.offset)
 223                                 return offset < other.offset;
 224                         if (width != other.width)
 225                                 return width < other.width;
 226                         return false;
 227                 }
 228         };
 229
 230         std::vector<int> modelExpressions;
 231         std::vector<bool> modelValues;
 232         std::set<ModelBlockInfo> modelInfo;
 233
 234         void generate_model()
 235         {
 236                 RTLIL::SigSpec modelSig;
 237                 modelExpressions.clear();
 238                 modelInfo.clear();
 239
 240                 // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals
 241
 242                 if (shows.size() == 0)
 243                 {
 244                         SigPool queued_signals, handled_signals, final_signals;
 245                         queued_signals = show_signal_pool;
 246                         while (queued_signals.size() > 0) {
 247                                 RTLIL::SigSpec sig = queued_signals.export_one();
 248                                 queued_signals.del(sig);
 249                                 handled_signals.add(sig);
 250                                 std::set<RTLIL::Cell*> drivers = show_drivers.find(sig);
 251                                 if (drivers.size() == 0) {
 252                                         final_signals.add(sig);
 253                                 } else {
 254                                         for (auto &d : drivers)
 255                                         for (auto &p : d->connections) {
 256                                                 if (d->type == "$dff" && p.first == "\\CLK")
 257                                                         continue;
 258                                                 if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
 259                                                         continue;
 260                                                 queued_signals.add(handled_signals.remove(sigmap(p.second)));
 261                                         }
 262                                 }
 263                         }
 264                         modelSig = final_signals.export_all();
 265
 266                         // additionally add all set and prove signals directly
 267                         // (it improves user confidence if we write the constraints back ;-)
 268                         modelSig.append(show_signal_pool.export_all());
 269                 }
 270                 else
 271                 {
 272                         for (auto &s : shows) {
 273                                 RTLIL::SigSpec sig;
 274                                 if (!RTLIL::SigSpec::parse(sig, module, s))
 275                                         log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str());
 276                                 log("Import show expression: %s\n", log_signal(sig));
 277                                 modelSig.append(sig);
 278                         }
 279                 }
 280
 281                 modelSig.sort_and_unify();
 282                 // log("Model signals: %s\n", log_signal(modelSig));
 283
 284                 for (auto &c : modelSig.chunks)
 285                         if (c.wire != NULL) {
 286                                 ModelBlockInfo info;
 287                                 RTLIL::SigSpec chunksig = c;
 288                                 info.width = chunksig.width;
 289                                 info.description = log_signal(chunksig);
 290
 291                                 for (int timestep = -1; timestep <= max_timestep; timestep++) {
 292                                         if ((timestep == -1 && max_timestep > 0) || timestep == 0)
 293                                                 continue;
 294                                         std::vector<int> vec = satgen.importSigSpec(chunksig, timestep);
 295                                         info.timestep = timestep;
 296                                         info.offset = modelExpressions.size();
 297                                         modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
 298                                         modelInfo.insert(info);
 299                                 }
 300                         }
 301
 302                 // Add zero step signals as collected by satgen
 303
 304                 modelSig = satgen.initial_state.export_all();
 305                 for (auto &c : modelSig.chunks)
 306                         if (c.wire != NULL) {
 307                                 ModelBlockInfo info;
 308                                 RTLIL::SigSpec chunksig = c;
 309                                 info.timestep = 0;
 310                                 info.offset = modelExpressions.size();
 311                                 info.width = chunksig.width;
 312                                 info.description = log_signal(chunksig);
 313                                 std::vector<int> vec = satgen.importSigSpec(chunksig, 1);
 314                                 modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
 315                                 modelInfo.insert(info);
 316                         }
 317         }
 318
 319         void print_model()
 320         {
 321                 int maxModelName = 10;
 322                 int maxModelWidth = 10;
 323
 324                 for (auto &info : modelInfo) {
 325                         maxModelName = std::max(maxModelName, int(info.description.size()));
 326                         maxModelWidth = std::max(maxModelWidth, info.width);
 327                 }
 328
 329                 log("\n");
 330
 331                 int last_timestep = -2;
 332                 for (auto &info : modelInfo)
 333                 {
 334                         RTLIL::Const value;
 335                         for (int i = 0; i < info.width; i++) {
 336                                 value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
 337                                 if (modelValues.size() == 2*modelExpressions.size() && modelValues.at(modelExpressions.size()+info.offset+i))
 338                                         value.bits.back() = RTLIL::State::Sx;
 339                         }
 340
 341                         if (info.timestep != last_timestep) {
 342                                 const char *hline = "---------------------------------------------------------------------------------------------------"
 343                                                     "---------------------------------------------------------------------------------------------------"
 344                                                     "---------------------------------------------------------------------------------------------------";
 345                                 if (last_timestep == -2) {
 346                                         log(max_timestep > 0 ? "  Time " : "  ");
 347                                         log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");
 348                                 }
 349                                 log(max_timestep > 0 ? "  ---- " : "  ");
 350                                 log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10,
 351                                                 hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline);
 352                                 last_timestep = info.timestep;
 353                         }
 354
 355                         if (max_timestep > 0) {
 356                                 if (info.timestep > 0)
 357                                         log("  %4d ", info.timestep);
 358                                 else
 359                                         log("  init ");
 360                         } else
 361                                 log("  ");
 362
 363                         if (info.width <= 32)
 364                                 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());
 365                         else
 366                                 log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str());
 367                 }
 368
 369                 if (last_timestep == -2)
 370                         log("  no model variables selected for display.\n");
 371         }
 372
 373         void invalidate_model()
 374         {
 375                 std::vector<int> clause;
 376                 for (size_t i = 0; i < modelExpressions.size(); i++)
 377                         clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i));
 378                 ez.assume(ez.expression(ezSAT::OpOr, clause));
 379         }
 380 };
 381
 382 } /* namespace */
 383
 384 static void print_proof_failed()
 385 {
 386         log("\n");
 387         log("   ______                   ___       ___       _ _            _ _ \n");
 388         log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
 389         log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
 390         log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
 391         log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
 392         log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
 393         log("\n");
 394 }
 395
 396 static void print_timeout()
 397 {
 398         log("\n");
 399         log("        _____  _  _      _____ ____  _     _____\n");
 400         log("       /__ __\\/ \\/ \\__/|/  __//  _ \\/ \\ /\\/__ __\\\n");
 401         log("         / \\  | || |\\/|||  \\  | / \\|| | ||  / \\\n");
 402         log("         | |  | || |  |||  /_ | \\_/|| \\_/|  | |\n");
 403         log("         \\_/  \\_/\\_/  \\|\\____\\\\____/\\____/  \\_/\n");
 404         log("\n");
 405 }
 406
 407 static void print_qed()
 408 {
 409         log("\n");
 410         log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
 411         log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
 412         log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
 413         log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
 414         log("                | $$  | $$    | $$__/       | $$  | $$   \n");
 415         log("                | $$/$$ $$    | $$          | $$  | $$   \n");
 416         log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
 417         log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
 418         log("                       \\__/                              \n");
 419         log("\n");
 420 }
 421
 422 struct SatPass : public Pass {
 423         SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
 424         virtual void help()
 425         {
 426                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 427                 log("\n");
 428                 log("    sat [options] [selection]\n");
 429                 log("\n");
 430                 log("This command solves a SAT problem defined over the currently selected circuit\n");
 431                 log("and additional constraints passed as parameters.\n");
 432                 log("\n");
 433                 log("    -all\n");
 434                 log("        show all solutions to the problem (this can grow exponentially, use\n");
 435                 log("        -max <N> instead to get <N> solutions)\n");
 436                 log("\n");
 437                 log("    -max <N>\n");
 438                 log("        like -all, but limit number of solutions to <N>\n");
 439                 log("\n");
 440                 log("    -set <signal> <value>\n");
 441                 log("        set the specified signal to the specified value.\n");
 442                 log("\n");
 443                 log("    -show <signal>\n");
 444                 log("        show the model for the specified signal. if no -show option is\n");
 445                 log("        passed then a set of signals to be shown is automatically selected.\n");
 446                 log("\n");
 447                 log("The following options can be used to set up a sequential problem:\n");
 448                 log("\n");
 449                 log("    -seq <N>\n");
 450                 log("        set up a sequential problem with <N> time steps. The steps will\n");
 451                 log("        be numbered from 1 to N.\n");
 452                 log("\n");
 453                 log("    -set-at <N> <signal> <value>\n");
 454                 log("    -unset-at <N> <signal>\n");
 455                 log("        set or unset the specified signal to the specified value in the\n");
 456                 log("        given timestep. this has priority over a -set for the same signal.\n");
 457                 log("\n");
 458                 log("The following additional options can be used to set up a proof. If also -seq\n");
 459                 log("is passed, a temporal induction proof is performed.\n");
 460                 log("\n");
 461                 log("    -prove <signal> <value>\n");
 462                 log("        Attempt to proof that <signal> is always <value>. In a temporal\n");
 463                 log("        induction proof it is proven that the condition holds forever after\n");
 464                 log("        the number of time steps passed using -seq.\n");
 465                 log("\n");
 466                 log("    -maxsteps <N>\n");
 467                 log("        Set a maximum length for the induction.\n");
 468                 log("\n");
 469                 log("    -timeout <N>\n");
 470                 log("        Maximum number of seconds a single SAT instance may take.\n");
 471                 log("\n");
 472                 log("    -verify\n");
 473                 log("        Return an error and stop the synthesis script if the proof fails.\n");
 474                 log("\n");
 475                 log("    -verify-no-timeout\n");
 476                 log("        Like -verify but do not return an error for timeouts.\n");
 477                 log("\n");
 478         }
 479         virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 480         {
 481                 std::vector<std::pair<std::string, std::string>> sets, prove;
 482                 std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 483                 std::map<int, std::vector<std::string>> unsets_at;
 484                 std::vector<std::string> shows;
 485                 int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
 486                 bool verify = false, fail_on_timeout = false;
 487
 488                 log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 489
 490                 size_t argidx;
 491                 for (argidx = 1; argidx < args.size(); argidx++) {
 492                         if (args[argidx] == "-all") {
 493                                 loopcount = -1;
 494                                 continue;
 495                         }
 496                         if (args[argidx] == "-verify") {
 497                                 fail_on_timeout = true;
 498                                 verify = true;
 499                                 continue;
 500                         }
 501                         if (args[argidx] == "-verify-no-timeout") {
 502                                 verify = true;
 503                                 continue;
 504                         }
 505                         if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
 506                                 timeout = atoi(args[++argidx].c_str());
 507                                 continue;
 508                         }
 509                         if (args[argidx] == "-max" && argidx+1 < args.size()) {
 510                                 loopcount = atoi(args[++argidx].c_str());
 511                                 continue;
 512                         }
 513                         if (args[argidx] == "-maxsteps" && argidx+1 < args.size()) {
 514                                 maxsteps = atoi(args[++argidx].c_str());
 515                                 continue;
 516                         }
 517                         if (args[argidx] == "-set" && argidx+2 < args.size()) {
 518                                 std::string lhs = args[++argidx].c_str();
 519                                 std::string rhs = args[++argidx].c_str();
 520                                 sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
 521                                 continue;
 522                         }
 523                         if (args[argidx] == "-prove" && argidx+2 < args.size()) {
 524                                 std::string lhs = args[++argidx].c_str();
 525                                 std::string rhs = args[++argidx].c_str();
 526                                 prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
 527                                 continue;
 528                         }
 529                         if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 530                                 seq_len = atoi(args[++argidx].c_str());
 531                                 continue;
 532                         }
 533                         if (args[argidx] == "-set-at" && argidx+3 < args.size()) {
 534                                 int timestep = atoi(args[++argidx].c_str());
 535                                 std::string lhs = args[++argidx].c_str();
 536                                 std::string rhs = args[++argidx].c_str();
 537                                 sets_at[timestep].push_back(std::pair<std::string, std::string>(lhs, rhs));
 538                                 continue;
 539                         }
 540                         if (args[argidx] == "-unset-at" && argidx+2 < args.size()) {
 541                                 int timestep = atoi(args[++argidx].c_str());
 542                                 std::string lhs = args[++argidx].c_str();
 543                                 unsets_at[timestep].push_back(lhs);
 544                                 continue;
 545                         }
 546                         if (args[argidx] == "-show" && argidx+1 < args.size()) {
 547                                 shows.push_back(args[++argidx]);
 548                                 continue;
 549                         }
 550                         break;
 551                 }
 552                 extra_args(args, argidx, design);
 553
 554                 RTLIL::Module *module = NULL;
 555                 for (auto &mod_it : design->modules)
 556                         if (design->selected(mod_it.second)) {
 557                                 if (module)
 558                                         log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n",
 559                                                         RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
 560                                 module = mod_it.second;
 561                         }
 562                 if (module == NULL)
 563                         log_cmd_error("Can't perform SAT on an empty selection!\n");
 564
 565                 if (prove.size() == 0 && verify)
 566                         log_cmd_error("Got -verify but nothing to prove!\n");
 567
 568                 if (prove.size() > 0 && seq_len > 0)
 569                 {
 570                         if (loopcount > 0)
 571                                 log_cmd_error("The options -max and -all are not supported for temporal induction proofs!\n");
 572
 573                         SatHelper basecase(design, module);
 574                         SatHelper inductstep(design, module);
 575
 576                         basecase.sets = sets;
 577                         basecase.prove = prove;
 578                         basecase.sets_at = sets_at;
 579                         basecase.unsets_at = unsets_at;
 580                         basecase.shows = shows;
 581                         basecase.timeout = timeout;
 582
 583                         for (int timestep = 1; timestep <= seq_len; timestep++)
 584                                 basecase.setup(timestep);
 585
 586                         inductstep.sets = sets;
 587                         inductstep.prove = prove;
 588                         inductstep.shows = shows;
 589                         inductstep.timeout = timeout;
 590
 591                         inductstep.setup(1);
 592                         inductstep.ez.assume(inductstep.setup_proof(1));
 593
 594                         for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
 595                         {
 596                                 log("\n** Trying induction with length %d **\n", inductlen);
 597
 598                                 // phase 1: proving base case
 599
 600                                 basecase.setup(seq_len + inductlen);
 601                                 int property = basecase.setup_proof(seq_len + inductlen);
 602                                 basecase.generate_model();
 603
 604                                 if (inductlen > 1)
 605                                         basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
 606
 607                                 log("\n[base case] Solving problem with %d variables and %d clauses..\n",
 608                                                 basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses());
 609
 610                                 if (basecase.solve(basecase.ez.NOT(property))) {
 611                                         log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
 612                                         print_proof_failed();
 613                                         basecase.print_model();
 614                                         goto tip_failed;
 615                                 }
 616
 617                                 if (basecase.gotTimeout)
 618                                         goto timeout;
 619
 620                                 log("Base case for induction length %d proven.\n", inductlen);
 621                                 basecase.ez.assume(property);
 622
 623                                 // phase 2: proving induction step
 624
 625                                 inductstep.setup(inductlen + 1);
 626                                 property = inductstep.setup_proof(inductlen + 1);
 627                                 inductstep.generate_model();
 628
 629                                 if (inductlen > 1)
 630                                         inductstep.force_unique_state(1, inductlen + 1);
 631
 632                                 log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
 633                                                 inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
 634
 635                                 if (!inductstep.solve(inductstep.ez.NOT(property))) {
 636                                         if (inductstep.gotTimeout)
 637                                                 goto timeout;
 638                                         log("Induction step proven: SUCCESS!\n");
 639                                         print_qed();
 640                                         goto tip_success;
 641                                 }
 642
 643                                 log("Induction step failed. Incrementing induction length.\n");
 644                                 inductstep.ez.assume(property);
 645
 646                                 inductstep.print_model();
 647                         }
 648
 649                         log("\nReached maximum number of time steps -> proof failed.\n");
 650                         print_proof_failed();
 651
 652                 tip_failed:
 653                         if (verify) {
 654                                 log("\n");
 655                                 log_error("Called with -verify and proof did fail!\n");
 656                         }
 657
 658                 tip_success:;
 659                 }
 660                 else
 661                 {
 662                         if (maxsteps > 0)
 663                                 log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
 664
 665                         SatHelper sathelper(design, module);
 666                         sathelper.sets = sets;
 667                         sathelper.prove = prove;
 668                         sathelper.sets_at = sets_at;
 669                         sathelper.unsets_at = unsets_at;
 670                         sathelper.shows = shows;
 671                         sathelper.timeout = timeout;
 672
 673                         if (seq_len == 0) {
 674                                 sathelper.setup();
 675                                 if (sathelper.prove.size() > 0)
 676                                         sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
 677                         } else {
 678                                 for (int timestep = 1; timestep <= seq_len; timestep++)
 679                                         sathelper.setup(timestep);
 680                         }
 681                         sathelper.generate_model();
 682
 683 #if 0
 684                         // print CNF for debugging
 685                         sathelper.ez.printDIMACS(stdout, true);
 686 #endif
 687
 688                         bool did_rerun = false;
 689
 690                 rerun_solver:
 691                         log("\nSolving problem with %d variables and %d clauses..\n",
 692                                         sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
 693
 694                         if (sathelper.solve())
 695                         {
 696                                 if (prove.size() == 0) {
 697                                         log("SAT solving finished - model found:\n");
 698                                 } else {
 699                                         log("SAT proof finished - model found: FAIL!\n");
 700                                         print_proof_failed();
 701                                 }
 702
 703                                 sathelper.print_model();
 704
 705                                 if (loopcount != 0) {
 706                                         loopcount--, did_rerun = true;
 707                                         sathelper.invalidate_model();
 708                                         goto rerun_solver;
 709                                 }
 710
 711                                 if (verify) {
 712                                         log("\n");
 713                                         log_error("Called with -verify and proof did fail!\n");
 714                                 }
 715                         }
 716                         else
 717                         {
 718                                 if (sathelper.gotTimeout)
 719                                         goto timeout;
 720                                 if (did_rerun)
 721                                         log("SAT solving finished - no more models found.\n");
 722                                 else if (prove.size() == 0)
 723                                         log("SAT solving finished - no model found.\n");
 724                                 else {
 725                                         log("SAT proof finished - no model found: SUCCESS!\n");
 726                                         print_qed();
 727                                 }
 728                         }
 729
 730                         if (verify && did_rerun) {
 731                                 log("\n");
 732                                 log_error("Called with -verify and proof did fail!\n");
 733                         }
 734                 }
 735
 736                 if (0) {
 737         timeout:
 738                         log("Interrupted SAT solver: TIMEOUT!\n");
 739                         print_timeout();
 740                         if (fail_on_timeout)
 741                                 log_error("Called with -verify and proof did time out!\n");
 742                 }
 743         }
 744 } SatPass;
 745