passes/sat/qbfsat.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2020  Alberto Gonzalez <boqwxp@airmail.cc>
   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 #include "kernel/yosys.h"
  21 #include "kernel/celltypes.h"
  22 #include "kernel/consteval.h"
  23 #include "kernel/log.h"
  24 #include "kernel/rtlil.h"
  25 #include "kernel/register.h"
  26 #include <cstdio>
  27 #include <algorithm>
  28
  29 #if defined(_WIN32)
  30 #  define WIFEXITED(x) 1
  31 #  define WIFSIGNALED(x) 0
  32 #  define WIFSTOPPED(x) 0
  33 #  define WEXITSTATUS(x) ((x) & 0xff)
  34 #  define WTERMSIG(x) SIGTERM
  35 #else
  36 #  include <sys/wait.h>
  37 #endif
  38
  39 USING_YOSYS_NAMESPACE
  40 PRIVATE_NAMESPACE_BEGIN
  41
  42 struct QbfSolutionType {
  43         std::vector<std::string> stdout_lines;
  44         dict<std::string, std::string> hole_to_value;
  45         bool sat;
  46         bool unknown; //true if neither 'sat' nor 'unsat'
  47
  48         QbfSolutionType() : sat(false), unknown(true) {}
  49 };
  50
  51 struct QbfSolveOptions {
  52         bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
  53         bool nooptimize, nobisection;
  54         bool sat, unsat, show_smtbmc;
  55         std::string specialize_soln_file;
  56         std::string write_soln_soln_file;
  57         std::string dump_final_smt2_file;
  58         size_t argidx;
  59         QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
  60                         nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
  61                         nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
  62                         argidx(0) {};
  63 };
  64
  65 void recover_solution(QbfSolutionType &sol) {
  66         YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
  67         YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
  68         YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
  69         YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
  70 #ifndef NDEBUG
  71         YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
  72         YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
  73 #endif
  74         YS_REGEX_MATCH_TYPE m;
  75         bool sat_regex_found = false;
  76         bool unsat_regex_found = false;
  77         dict<std::string, bool> hole_value_recovered;
  78         for (const std::string &x : sol.stdout_lines) {
  79                 if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
  80                         std::string loc = m[1].str();
  81                         std::string val = m[2].str();
  82 #ifndef NDEBUG
  83                         log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
  84                         log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
  85 #endif
  86                         sol.hole_to_value[loc] = val;
  87                 }
  88                 else if (YS_REGEX_NS::regex_search(x, sat_regex))
  89                         sat_regex_found = true;
  90                 else if (YS_REGEX_NS::regex_search(x, unsat_regex))
  91                         unsat_regex_found = true;
  92                 else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
  93                         sol.unknown = true;
  94                         log_warning("solver ran out of memory\n");
  95                 }
  96         }
  97 #ifndef NDEBUG
  98         log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
  99         log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
 100 #endif
 101 }
 102
 103 dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) {
 104         dict<std::string, std::string> hole_loc_to_name;
 105         for (auto cell : module->cells()) {
 106                 std::string cell_src = cell->get_src_attribute();
 107                 auto pos = sol.hole_to_value.find(cell_src);
 108                 if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
 109                         log_assert(hole_loc_to_name.find(pos->first) == hole_loc_to_name.end());
 110                         hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str();
 111                 }
 112         }
 113
 114         return hole_loc_to_name;
 115 }
 116
 117 pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
 118         bool found_input = false;
 119         bool found_hole = false;
 120         bool found_1bit_output = false;
 121         bool found_assert_assume = false;
 122         pool<std::string> input_wires;
 123         for (auto wire : module->wires()) {
 124                 if (wire->port_input) {
 125                         found_input = true;
 126                         input_wires.insert(wire->name.str());
 127                 }
 128                 if (wire->port_output && wire->width == 1)
 129                         found_1bit_output = true;
 130         }
 131         for (auto cell : module->cells()) {
 132                 if (cell->type == "$allconst")
 133                         found_input = true;
 134                 if (cell->type == "$anyconst")
 135                         found_hole = true;
 136                 if (cell->type.in("$assert", "$assume"))
 137                         found_assert_assume = true;
 138         }
 139         if (!found_input)
 140                 log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
 141         if (!found_hole)
 142                 log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
 143         if (!found_1bit_output && !found_assert_assume)
 144                 log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
 145         if (!found_assert_assume && !opt.assume_outputs)
 146                 log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
 147
 148         return input_wires;
 149 }
 150
 151 void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) {
 152         std::ofstream fout(file.c_str());
 153         if (!fout)
 154                 log_cmd_error("could not open solution file for writing.\n");
 155
 156         dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
 157         for(auto &x : sol.hole_to_value)
 158                 fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl;
 159 }
 160
 161 void specialize_from_file(RTLIL::Module *module, const std::string &file) {
 162         YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$");
 163         YS_REGEX_MATCH_TYPE m;
 164         pool<RTLIL::Cell *> anyconsts_to_remove;
 165         dict<std::string, std::string> hole_name_to_value;
 166         std::ifstream fin(file.c_str());
 167         if (!fin)
 168                 log_cmd_error("could not read solution file.\n");
 169
 170         std::string buf;
 171         while (std::getline(fin, buf)) {
 172                 log_assert(YS_REGEX_NS::regex_search(buf, m, hole_assn_regex));
 173                 std::string hole_name = m[1].str();
 174                 std::string hole_value = m[2].str();
 175                 hole_name_to_value[hole_name] = hole_value;
 176         }
 177
 178         for (auto cell : module->cells())
 179                 if (cell->type == "$anyconst") {
 180                         auto anyconst_port_y = cell->getPort(ID::Y).as_wire();
 181                         if (anyconst_port_y == nullptr)
 182                                 continue;
 183                         if (hole_name_to_value.find(anyconst_port_y->name.str()) != hole_name_to_value.end())
 184                                 anyconsts_to_remove.insert(cell);
 185                 }
 186         for (auto cell : anyconsts_to_remove)
 187                 module->remove(cell);
 188
 189         for (auto &it : hole_name_to_value) {
 190                 std::string hole_name = it.first;
 191                 std::string hole_value = it.second;
 192                 RTLIL::Wire *wire = module->wire(hole_name);
 193 #ifndef NDEBUG
 194                 log_assert(wire != nullptr);
 195                 log_assert(wire->width > 0 && GetSize(hole_value) == wire->width);
 196 #endif
 197
 198                 log("Specializing %s from file with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
 199                 std::vector<RTLIL::SigBit> value_bv;
 200                 value_bv.reserve(wire->width);
 201                 for (char c : hole_value)
 202                         value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
 203                 std::reverse(value_bv.begin(), value_bv.end());
 204                 module->connect(wire, value_bv);
 205         }
 206 }
 207
 208 void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) {
 209         dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
 210         pool<RTLIL::Cell *> anyconsts_to_remove;
 211         for (auto cell : module->cells())
 212                 if (cell->type == "$anyconst")
 213                         if (hole_loc_to_name.find(cell->get_src_attribute()) != hole_loc_to_name.end())
 214                                 anyconsts_to_remove.insert(cell);
 215         for (auto cell : anyconsts_to_remove)
 216                 module->remove(cell);
 217         for (auto &it : sol.hole_to_value) {
 218                 std::string hole_loc = it.first;
 219                 std::string hole_value = it.second;
 220
 221 #ifndef NDEBUG
 222                 auto pos = hole_loc_to_name.find(hole_loc);
 223                 log_assert(pos != hole_loc_to_name.end());
 224 #endif
 225
 226                 std::string hole_name = hole_loc_to_name[hole_loc];
 227                 RTLIL::Wire *wire = module->wire(hole_name);
 228 #ifndef NDEBUG
 229                 log_assert(wire != nullptr);
 230                 log_assert(wire->width > 0 && GetSize(hole_value) == wire->width);
 231 #endif
 232
 233                 if (!quiet)
 234                         log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
 235                 std::vector<RTLIL::SigBit> value_bv;
 236                 value_bv.reserve(wire->width);
 237                 for (char c : hole_value)
 238                         value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
 239                 std::reverse(value_bv.begin(), value_bv.end());
 240                 module->connect(wire, value_bv);
 241         }
 242 }
 243
 244 void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) {
 245         log("Satisfiable model:\n");
 246         dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
 247         for (auto &it : sol.hole_to_value) {
 248                 std::string hole_loc = it.first;
 249                 std::string hole_value = it.second;
 250
 251 #ifndef NDEBUG
 252                 auto pos = hole_loc_to_name.find(hole_loc);
 253                 log_assert(pos != hole_loc_to_name.end());
 254 #endif
 255
 256                 std::string hole_name = hole_loc_to_name[hole_loc];
 257                 log("\t%s = %lu'b%s\n", hole_name.c_str(), hole_value.size(), hole_value.c_str());
 258                 std::vector<RTLIL::SigBit> value_bv;
 259                 value_bv.reserve(hole_value.size());
 260                 for (char c : hole_value)
 261                         value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
 262                 std::reverse(value_bv.begin(), value_bv.end());
 263         }
 264 }
 265
 266 void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) {
 267         for (auto &n : input_wires) {
 268                 RTLIL::Wire *input = module->wire(n);
 269 #ifndef NDEBUG
 270                 log_assert(input != nullptr);
 271 #endif
 272
 273                 RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst");
 274                 allconst->setParam(ID(WIDTH), input->width);
 275                 allconst->setPort(ID::Y, input);
 276                 allconst->set_src_attribute(input->get_src_attribute());
 277                 input->port_input = false;
 278                 log("Replaced input %s with $allconst cell.\n", n.c_str());
 279         }
 280         module->fixup_ports();
 281 }
 282
 283 void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
 284         std::vector<RTLIL::Wire *> wires_to_assume;
 285         for (auto w : module->wires())
 286                 if (w->port_output && w->width == 1)
 287                         wires_to_assume.push_back(w);
 288
 289         if (wires_to_assume.size() == 0)
 290                 return;
 291         else {
 292                 log("Adding $assume cell for output(s): ");
 293                 for (auto w : wires_to_assume)
 294                         log("\"%s\" ", w->name.c_str());
 295                 log("\n");
 296         }
 297
 298         if (opt.assume_neg) {
 299                 for (unsigned int i = 0; i < wires_to_assume.size(); ++i) {
 300                         RTLIL::SigSpec n_wire = module->LogicNot(wires_to_assume[i]->name.str() + "__n__qbfsat", wires_to_assume[i], false, wires_to_assume[i]->get_src_attribute());
 301                         wires_to_assume[i] = n_wire.as_wire();
 302                 }
 303         }
 304
 305         for (auto i = 0; wires_to_assume.size() > 1; ++i) {
 306                 std::vector<RTLIL::Wire *> buf;
 307                 for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) {
 308                         std::stringstream strstr; strstr << i << "_" << j;
 309                         RTLIL::Wire *and_wire = module->addWire("\\_qbfsat_and_" + strstr.str(), 1);
 310                         module->addLogicAnd("$_qbfsat_and_" + strstr.str(), wires_to_assume[j], wires_to_assume[j+1], and_wire, false, wires_to_assume[j]->get_src_attribute());
 311                         buf.push_back(and_wire);
 312                 }
 313                 if (wires_to_assume.size() % 2 == 1)
 314                         buf.push_back(wires_to_assume[wires_to_assume.size() - 1]);
 315                 wires_to_assume.swap(buf);
 316         }
 317
 318 #ifndef NDEBUG
 319         log_assert(wires_to_assume.size() == 1);
 320 #endif
 321         module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1);
 322 }
 323
 324 QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, const std::string &tempdir_name, const bool quiet = false, const int iter_num = 0) {
 325         //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
 326         QbfSolutionType ret;
 327         const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
 328         const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2";
 329         const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
 330         const std::string smtbmc_warning = "z3: WARNING:";
 331         const bool show_smtbmc = opt.show_smtbmc;
 332
 333         Pass::call(mod->design, smt2_command);
 334
 335         auto process_line = [&ret, &smtbmc_warning, &show_smtbmc, &quiet](const std::string &line) {
 336                 ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline
 337                 auto warning_pos = line.find(smtbmc_warning);
 338                 if (warning_pos != std::string::npos)
 339                         log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());
 340                 else
 341                         if (show_smtbmc && !quiet)
 342                                 log("smtbmc output: %s", line.c_str());
 343         };
 344         log_header(mod->design, "Solving QBF-SAT problem.\n");
 345         if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str());
 346         int retval = run_command(smtbmc_cmd, process_line);
 347         if (retval == 0) {
 348                 ret.sat = true;
 349                 ret.unknown = false;
 350         } else if (retval == 1) {
 351                 ret.sat = false;
 352                 ret.unknown = false;
 353         }
 354
 355         recover_solution(ret);
 356         return ret;
 357 }
 358
 359 QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
 360         QbfSolutionType ret, best_soln;
 361         const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX");
 362         RTLIL::Module *module = mod;
 363         RTLIL::Design *design = module->design;
 364         std::string module_name = module->name.str();
 365         RTLIL::Wire *wire_to_optimize = nullptr;
 366         RTLIL::IdString wire_to_optimize_name;
 367         bool maximize = false;
 368         log_assert(module->design != nullptr);
 369
 370         Pass::call(design, "design -push-copy");
 371
 372         //Replace input wires with wires assigned $allconst cells:
 373         pool<std::string> input_wires = validate_design_and_get_inputs(module, opt);
 374         allconstify_inputs(module, input_wires);
 375         if (opt.assume_outputs)
 376                 assume_miter_outputs(module, opt);
 377
 378         //Find the wire to be optimized, if any:
 379         for (auto wire : module->wires())
 380                 if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize"))
 381                         wire_to_optimize = wire;
 382         if (wire_to_optimize != nullptr) {
 383                 wire_to_optimize_name = wire_to_optimize->name;
 384                 maximize = wire_to_optimize->get_bool_attribute("\\maximize");
 385         }
 386
 387         if (opt.nobisection || opt.nooptimize) {
 388                 if (wire_to_optimize != nullptr && opt.nooptimize) {
 389                         wire_to_optimize->set_bool_attribute("\\maximize", false);
 390                         wire_to_optimize->set_bool_attribute("\\minimize", false);
 391                 }
 392                 ret = call_qbf_solver(module, opt, tempdir_name, false, 0);
 393         } else {
 394                 //Do the iterated bisection method:
 395                 unsigned int iter_num = 1;
 396                 unsigned int success = 0;
 397                 unsigned int failure = 0;
 398                 unsigned int cur_thresh = 0;
 399
 400                 log_assert(wire_to_optimize != nullptr);
 401                 log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize));
 402
 403                 //If maximizing, grow until we get a failure.  Then bisect success and failure.
 404                 while (failure == 0 || success - failure > 1) {
 405                         Pass::call(design, "design -push-copy");
 406                         log_header(design, "Preparing QBF-SAT problem.\n");
 407
 408                         if (cur_thresh != 0) {
 409                                 //Add thresholding logic (but not on the initial run when we don't have a sense of where to start):
 410                                 RTLIL::SigSpec comparator = maximize? module->Ge(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false)
 411                                                                     : module->Le(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false);
 412
 413                                 module->addAssume(wire_to_optimize_name.str() + "__threshold", comparator, RTLIL::Const(1, 1));
 414                                 log("Trying to solve with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), cur_thresh);
 415                         }
 416
 417                         ret = call_qbf_solver(module, opt, tempdir_name, false, iter_num);
 418                         Pass::call(design, "design -pop");
 419                         module = design->module(module_name);
 420
 421                         if (!ret.unknown && ret.sat) {
 422                                 Pass::call(design, "design -push-copy");
 423                                 specialize(module, ret, true);
 424
 425                                 RTLIL::SigSpec wire, value, undef;
 426                                 RTLIL::SigSpec::parse_sel(wire, design, module, wire_to_optimize_name.str());
 427
 428                                 ConstEval ce(module);
 429                                 value = wire;
 430                                 if (!ce.eval(value, undef))
 431                                         log_cmd_error("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(wire), log_signal(undef));
 432                                 log_assert(value.is_fully_const());
 433                                 success = value.as_const().as_int();
 434                                 best_soln = ret;
 435                                 log("Problem is satisfiable with %s = %d.\n", wire_to_optimize_name.c_str(), success);
 436                                 Pass::call(design, "design -pop");
 437                                 module = design->module(module_name);
 438
 439                                 //sometimes this happens if we get an 'unknown' or timeout
 440                                 if (!maximize && success < failure)
 441                                         break;
 442                                 else if (maximize && success > failure)
 443                                         break;
 444                         } else {
 445                                 //Treat 'unknown' as UNSAT
 446                                 failure = cur_thresh;
 447                                 if (failure == 0) {
 448                                         log("Problem is NOT satisfiable.\n");
 449                                         break;
 450                                 }
 451                                 else
 452                                         log("Problem is NOT satisfiable with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), failure);
 453                         }
 454
 455                         iter_num++;
 456                         cur_thresh = (maximize && failure == 0)? 2 * success //growth
 457                                                                : (success + failure) / 2; //bisection
 458                 }
 459                 if (success != 0 || failure != 0) {
 460                         log("Wire %s is %s at %d.\n", wire_to_optimize_name.c_str(), (maximize? "maximized" : "minimized"), success);
 461                         ret = best_soln;
 462                 }
 463         }
 464
 465         if(!opt.nocleanup)
 466                 remove_directory(tempdir_name);
 467
 468         Pass::call(design, "design -pop");
 469
 470         return ret;
 471 }
 472
 473 QbfSolveOptions parse_args(const std::vector<std::string> &args) {
 474         QbfSolveOptions opt;
 475         for (opt.argidx = 1; opt.argidx < args.size(); opt.argidx++) {
 476                 if (args[opt.argidx] == "-nocleanup") {
 477                         opt.nocleanup = true;
 478                         continue;
 479                 }
 480                 else if (args[opt.argidx] == "-specialize") {
 481                         opt.specialize = true;
 482                         continue;
 483                 }
 484                 else if (args[opt.argidx] == "-assume-outputs") {
 485                         opt.assume_outputs = true;
 486                         continue;
 487                 }
 488                 else if (args[opt.argidx] == "-assume-negative-polarity") {
 489                         opt.assume_neg = true;
 490                         continue;
 491                 }
 492                 else if (args[opt.argidx] == "-nooptimize") {
 493                         opt.nooptimize = true;
 494                         continue;
 495                 }
 496                 else if (args[opt.argidx] == "-nobisection") {
 497                         opt.nobisection = true;
 498                         continue;
 499                 }
 500                 else if (args[opt.argidx] == "-sat") {
 501                         opt.sat = true;
 502                         continue;
 503                 }
 504                 else if (args[opt.argidx] == "-unsat") {
 505                         opt.unsat = true;
 506                         continue;
 507                 }
 508                 else if (args[opt.argidx] == "-show-smtbmc") {
 509                         opt.show_smtbmc = true;
 510                         continue;
 511                 }
 512                 else if (args[opt.argidx] == "-dump-final-smt2") {
 513                         opt.dump_final_smt2 = true;
 514                         if (args.size() <= opt.argidx + 1)
 515                                 log_cmd_error("smt2 file not specified.\n");
 516                         else
 517                                 opt.dump_final_smt2_file = args[++opt.argidx];
 518                         continue;
 519                 }
 520                 else if (args[opt.argidx] == "-specialize-from-file") {
 521                         opt.specialize_from_file = true;
 522                         if (args.size() <= opt.argidx + 1)
 523                                 log_cmd_error("solution file not specified.\n");
 524                         else
 525                                 opt.specialize_soln_file = args[++opt.argidx];
 526                         continue;
 527                 }
 528                 else if (args[opt.argidx] == "-write-solution") {
 529                         opt.write_solution = true;
 530                         if (args.size() <= opt.argidx + 1)
 531                                 log_cmd_error("solution file not specified.\n");
 532                         else
 533                                 opt.write_soln_soln_file = args[++opt.argidx];
 534                         continue;
 535                 }
 536                 break;
 537         }
 538
 539         return opt;
 540 }
 541
 542 void print_proof_failed()
 543 {
 544         log("\n");
 545         log("   ______                   ___       ___       _ _            _ _ \n");
 546         log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
 547         log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
 548         log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
 549         log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
 550         log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
 551         log("\n");
 552 }
 553
 554 void print_qed()
 555 {
 556         log("\n");
 557         log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
 558         log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
 559         log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
 560         log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
 561         log("                | $$  | $$    | $$__/       | $$  | $$   \n");
 562         log("                | $$/$$ $$    | $$          | $$  | $$   \n");
 563         log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
 564         log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
 565         log("                       \\__/                              \n");
 566         log("\n");
 567 }
 568
 569 struct QbfSatPass : public Pass {
 570         QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
 571         void help() YS_OVERRIDE
 572         {
 573                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 574                 log("\n");
 575                 log("    qbfsat [options] [selection]\n");
 576                 log("\n");
 577                 log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
 578                 log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
 579                 log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
 580                 log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
 581                 log("by default.\n");
 582                 log("\n");
 583                 log("    -nocleanup\n");
 584                 log("        Do not delete temporary files and directories.  Useful for\n");
 585                 log("        debugging.\n");
 586                 log("\n");
 587                 log("    -dump-final-smt2 <file>\n");
 588                 log("        Pass the --dump-smt2 option to yosys-smtbmc.\n");
 589                 log("\n");
 590                 log("    -assume-outputs\n");
 591                 log("        Add an $assume cell for the conjunction of all one-bit module output wires.\n");
 592                 log("\n");
 593                 log("    -assume-negative-polarity\n");
 594                 log("        When adding $assume cells for one-bit module output wires, assume they are\n");
 595                 log("        negative polarity signals and should always be low, for example like the\n");
 596                 log("        miters created with the `miter` command.\n");
 597                 log("\n");
 598                 log("    -nooptimize\n");
 599                 log("        Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n");
 600                 log("        \"(minimize)\" in the SMTLIBv2, and generally make no attempt to optimize anything.\n");
 601                 log("\n");
 602                 log("    -nobisection\n");
 603                 log("        If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n");
 604                 log("        attempt to optimize that value with the default iterated solving and threshold\n");
 605                 log("        bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n");
 606                 log("        command in the SMTLIBv2 output and hope that the solver supports optimizing\n");
 607                 log("        quantified bitvector problems.\n");
 608                 log("\n");
 609                 log("    -sat\n");
 610                 log("        Generate an error if the solver does not return \"sat\".\n");
 611                 log("\n");
 612                 log("    -unsat\n");
 613                 log("        Generate an error if the solver does not return \"unsat\".\n");
 614                 log("\n");
 615                 log("    -show-smtbmc\n");
 616                 log("        Print the output from yosys-smtbmc.\n");
 617                 log("\n");
 618                 log("    -specialize\n");
 619                 log("        Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
 620                 log("\n");
 621                 log("    -specialize-from-file <solution file>\n");
 622                 log("        Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
 623                 log("        cells in the current module with values provided by the specified file.\n");
 624                 log("\n");
 625                 log("    -write-solution <solution file>\n");
 626                 log("        Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
 627                 log("        to the specified file.");
 628                 log("\n");
 629                 log("\n");
 630         }
 631
 632         void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 633         {
 634                 log_header(design, "Executing QBFSAT pass (solving QBF-SAT problems in the circuit).\n");
 635                 QbfSolveOptions opt = parse_args(args);
 636                 extra_args(args, opt.argidx, design);
 637
 638                 RTLIL::Module *module = nullptr;
 639                 for (auto mod : design->selected_modules()) {
 640                         if (module)
 641                                 log_cmd_error("Only one module must be selected for the QBF-SAT pass! (selected: %s and %s)\n", log_id(module), log_id(mod));
 642                         module = mod;
 643                 }
 644                 if (module == nullptr)
 645                         log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");
 646
 647                 log_push();
 648                 if (!opt.specialize_from_file) {
 649                         //Save the design to restore after modiyfing the current module.
 650                         std::string module_name = module->name.str();
 651
 652                         QbfSolutionType ret = qbf_solve(module, opt);
 653                         module = design->module(module_name);
 654                         if (ret.unknown) {
 655                                 log_warning("solver did not give an answer\n");
 656                                 if (opt.sat || opt.unsat)
 657                                         log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT");
 658                         }
 659                         else if (ret.sat) {
 660                                 print_qed();
 661                                 if (opt.write_solution) {
 662                                         write_solution(module, ret, opt.write_soln_soln_file);
 663                                 }
 664                                 if (opt.specialize) {
 665                                         specialize(module, ret);
 666                                 } else {
 667                                         dump_model(module, ret);
 668                                 }
 669                                 if (opt.unsat)
 670                                         log_cmd_error("expected problem to be UNSAT\n");
 671                         }
 672                         else {
 673                                 print_proof_failed();
 674                                 if (opt.sat)
 675                                         log_cmd_error("expected problem to be SAT\n");
 676                         }
 677                 } else
 678                         specialize_from_file(module, opt.specialize_soln_file);
 679                 log_pop();
 680         }
 681 } QbfSatPass;
 682
 683 PRIVATE_NAMESPACE_END