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/log.h"
  23 #include "kernel/rtlil.h"
  24 #include "kernel/register.h"
  25 #include <cstdio>
  26
  27 #if defined(_WIN32)
  28 #  define WIFEXITED(x) 1
  29 #  define WIFSIGNALED(x) 0
  30 #  define WIFSTOPPED(x) 0
  31 #  define WEXITSTATUS(x) ((x) & 0xff)
  32 #  define WTERMSIG(x) SIGTERM
  33 #else
  34 #  include <sys/wait.h>
  35 #endif
  36
  37 USING_YOSYS_NAMESPACE
  38 PRIVATE_NAMESPACE_BEGIN
  39
  40 struct QbfSolutionType {
  41         std::vector<std::string> stdout;
  42         std::map<std::string, std::string> hole_to_value;
  43         bool sat;
  44         bool unknown; //true if neither 'sat' nor 'unsat'
  45         bool success; //true if exit code 0
  46
  47         QbfSolutionType() : sat(false), unknown(true), success(false) {}
  48 };
  49
  50 struct QbfSolveOptions {
  51         bool timeout, specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2;
  52         long timeout_sec;
  53         std::string specialize_soln_file;
  54         std::string write_soln_soln_file;
  55         std::string dump_final_smt2_file;
  56         QbfSolveOptions() : timeout(false), specialize(false), specialize_from_file(false), write_solution(false),
  57                                 nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {};
  58 };
  59
  60 void recover_solution(RTLIL::Module *mod, QbfSolutionType &sol) {
  61         YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
  62         YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
  63         YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
  64         YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
  65         YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
  66         YS_REGEX_MATCH_TYPE m;
  67         bool sat_regex_found = false;
  68         bool unsat_regex_found = false;
  69         std::map<std::string, bool> hole_value_recovered;
  70         for (const std::string &x : sol.stdout) {
  71                 if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
  72                         std::string loc = m[1].str();
  73                         std::string val = m[2].str();
  74                         log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
  75                         log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
  76                         sol.hole_to_value[loc] = val;
  77                 }
  78                 else if (YS_REGEX_NS::regex_search(x, sat_regex))
  79                         sat_regex_found = true;
  80                 else if (YS_REGEX_NS::regex_search(x, unsat_regex))
  81                         unsat_regex_found = true;
  82         }
  83         log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
  84         log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
  85 }
  86
  87 QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
  88         QbfSolutionType ret;
  89         std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
  90         std::string smtbmc_warning = "z3: WARNING:";
  91
  92         std::string tempdir_name = "/tmp/yosys-z3-XXXXXX";
  93         tempdir_name = make_temp_dir(tempdir_name);
  94         std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2";
  95         log_assert(mod->design != nullptr);
  96         Pass::call(mod->design, smt2_command);
  97
  98         //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g [--dump-smt2 <file>]`
  99         {
 100                 fflush(stdout);
 101                 bool keep_reading = true;
 102                 int status = 0;
 103                 int retval = 0;
 104                 char buf[1024] = {0};
 105                 std::string linebuf = "";
 106                 std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1";
 107                 log("Launching \"%s\".\n", cmd.c_str());
 108
 109 #ifndef EMSCRIPTEN
 110                 FILE *f = popen(cmd.c_str(), "r");
 111                 if (f == nullptr)
 112                         log_cmd_error("errno %d after popen() returned NULL.\n", errno);
 113                 while (keep_reading) {
 114                         keep_reading = (fgets(buf, sizeof(buf), f) != nullptr);
 115                         linebuf += buf;
 116                         memset(buf, 0, sizeof(buf));
 117
 118                         auto pos = linebuf.find('\n');
 119                         while (pos != std::string::npos) {
 120                                 std::string line = linebuf.substr(0, pos);
 121                                 linebuf.erase(0, pos + 1);
 122                                 ret.stdout.push_back(line);
 123                                 auto warning_pos = line.find(smtbmc_warning);
 124                                 if(warning_pos != std::string::npos)
 125                                         log_warning("%s\n", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());
 126                                 else
 127                                         log("smtbmc output: %s\n", line.c_str());
 128
 129                                 pos = linebuf.find('\n');
 130                         }
 131                 }
 132                 status = pclose(f);
 133 #endif
 134
 135                 if(WIFEXITED(status)) {
 136                     retval = WEXITSTATUS(status);
 137                 }
 138                 else if(WIFSIGNALED(status)) {
 139                     retval = WTERMSIG(status);
 140                 }
 141                 else if(WIFSTOPPED(status)) {
 142                     retval = WSTOPSIG(status);
 143                 }
 144
 145                 if (retval == 0) {
 146                         ret.sat = true;
 147                         ret.unknown = false;
 148                 } else if (retval == 1) {
 149                         ret.sat = false;
 150                         ret.unknown = false;
 151                 }
 152         }
 153
 154         if(!opt.nocleanup)
 155                 remove_directory(tempdir_name);
 156
 157         recover_solution(mod, ret);
 158
 159         return ret;
 160 }
 161
 162
 163 void print_proof_failed()
 164 {
 165         log("\n");
 166         log("   ______                   ___       ___       _ _            _ _ \n");
 167         log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
 168         log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
 169         log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
 170         log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
 171         log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
 172         log("\n");
 173 }
 174
 175 void print_qed()
 176 {
 177         log("\n");
 178         log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
 179         log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
 180         log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
 181         log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
 182         log("                | $$  | $$    | $$__/       | $$  | $$   \n");
 183         log("                | $$/$$ $$    | $$          | $$  | $$   \n");
 184         log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
 185         log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
 186         log("                       \\__/                              \n");
 187         log("\n");
 188 }
 189
 190 struct QbfSatPass : public Pass {
 191         QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
 192         void help() YS_OVERRIDE
 193         {
 194                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 195                 log("\n");
 196                 log("    qbfsat [options] [selection]\n");
 197                 log("\n");
 198                 log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
 199                 log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
 200                 log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
 201                 log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
 202                 log("by default.\n");
 203                 log("\n");
 204                 log("    -timeout <seconds>\n");
 205                 log("        Set the solver timeout to the specified number of seconds.\n");
 206                 log("\n");
 207                 log("    -nocleanup\n");
 208                 log("        Do not delete temporary files and directories.  Useful for\n");
 209                 log("        debugging.\n");
 210                 log("\n");
 211                 log("    -dump-final-smt2 <file>\n");
 212                 log("        Pass the --dump-smt2 option to yosys-smtbmc.\n");
 213                 log("\n");
 214                 log("    -specialize\n");
 215                 log("        Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
 216                 log("\n");
 217                 log("    -specialize-from-file <solution file>\n");
 218                 log("        Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
 219                 log("        cells in the current module with values provided by the specified file.\n");
 220                 log("\n");
 221                 log("    -write-solution <solution file>\n");
 222                 log("        Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
 223                 log("        to the specified file.");
 224                 log("\n");
 225                 log("\n");
 226         }
 227         void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 228         {
 229                 QbfSolveOptions opt;
 230                 log_header(design, "Executing QBF-SAT pass (solving QBF-SAT problems in the circuit).\n");
 231
 232                 size_t argidx;
 233                 for (argidx = 1; argidx < args.size(); argidx++) {
 234                         if (args[argidx] == "-timeout") {
 235                                 opt.timeout = true;
 236                                 if (args.size() <= argidx + 1)
 237                                         log_cmd_error("timeout not specified.\n");
 238                                 else
 239                                         opt.timeout_sec = atol(args[++argidx].c_str());
 240                                 continue;
 241                         }
 242                         else if (args[argidx] == "-nocleanup") {
 243                                 opt.nocleanup = true;
 244                                 continue;
 245                         }
 246                         else if (args[argidx] == "-specialize") {
 247                                 opt.specialize = true;
 248                                 continue;
 249                         }
 250                         else if (args[argidx] == "-dump-final-smt2") {
 251                                 opt.dump_final_smt2 = true;
 252                                 if (args.size() <= argidx + 1)
 253                                         log_cmd_error("smt2 file not specified.\n");
 254                                 else
 255                                         opt.dump_final_smt2_file = args[++argidx];
 256                                 continue;
 257                         }
 258                         else if (args[argidx] == "-specialize-from-file") {
 259                                 opt.specialize_from_file = true;
 260                                 if (args.size() <= argidx + 1)
 261                                         log_cmd_error("solution file not specified.\n");
 262                                 else
 263                                         opt.specialize_soln_file = args[++argidx];
 264                                 continue;
 265                         }
 266                         else if (args[argidx] == "-write-solution") {
 267                                 opt.write_solution = true;
 268                                 if (args.size() <= argidx + 1)
 269                                         log_cmd_error("solution file not specified.\n");
 270                                 else
 271                                         opt.write_soln_soln_file = args[++argidx];
 272                                 continue;
 273                         }
 274                         break;
 275                 }
 276                 extra_args(args, argidx, design);
 277
 278                 RTLIL::Module *module = NULL;
 279                 for (auto mod : design->selected_modules()) {
 280                         if (module)
 281                                 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));
 282                         module = mod;
 283                 }
 284                 if (module == NULL)
 285                         log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");
 286
 287                 bool found_input = false;
 288                 bool found_hole = false;
 289                 bool found_1bit_output = false;
 290                 std::set<std::string> input_wires;
 291                 for (auto wire : module->wires()) {
 292                         if (wire->port_input) {
 293                                 found_input = true;
 294                                 input_wires.insert(wire->name.str());
 295                         }
 296                         if (wire->port_output && wire->width == 1)
 297                                 found_1bit_output = true;
 298                 }
 299                 for (auto cell : module->cells()) {
 300                         if (cell->type == "$allconst")
 301                                 found_input = true;
 302                         if (cell->type == "$anyconst")
 303                                 found_hole = true;
 304                         if (cell->type.in("$assert", "$assume"))
 305                                 found_1bit_output = true;
 306                 }
 307                 if (!found_input)
 308                         log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
 309                 if (!found_hole)
 310                         log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
 311                 if (!found_1bit_output)
 312                         log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s.  Is this a miter circuit?\n");
 313
 314                 //Save the design to restore after modiyfing the current module.
 315                 std::string module_name = module->name.str();
 316                 Pass::call(design, "design -save _qbfsat_tmp");
 317
 318                 //Replace input wires with wires assigned $allconst cells.
 319                 for(auto &n : input_wires) {
 320                         RTLIL::Wire *input = module->wire(n);
 321                         log_assert(input != nullptr);
 322
 323                         RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst");
 324                         allconst->setParam(ID(WIDTH), input->width);
 325                         allconst->setPort(ID::Y, input);
 326                         allconst->set_src_attribute(input->get_src_attribute());
 327                         input->port_input = false;
 328                         log("Replaced input %s with $allconst cell.\n", n.c_str());
 329                 }
 330                 module->fixup_ports();
 331
 332                 QbfSolutionType ret = qbf_solve(module, opt);
 333                 Pass::call(design, "design -load _qbfsat_tmp");
 334                 module = design->module(module_name);
 335
 336                 if (ret.unknown)
 337                         log_warning("solver did not give an answer\n");
 338                 else if (ret.sat)
 339                         print_qed();
 340                 else
 341                         print_proof_failed();
 342
 343                 if (opt.specialize) {
 344                         std::map<std::string, std::string> hole_loc_to_name;
 345                         for (auto cell : module->cells()) {
 346                                 std::string cell_src = cell->get_src_attribute();
 347                                 auto pos = ret.hole_to_value.find(cell_src);
 348                                 if (pos != ret.hole_to_value.end()) {
 349                                         log_assert(cell->type.in("$anyconst", "$anyseq"));
 350                                         log_assert(cell->hasPort(ID::Y));
 351                                         log_assert(cell->getPort(ID::Y).is_wire());
 352                                         hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str();
 353                                 }
 354                         }
 355                         for (auto &it : ret.hole_to_value) {
 356                                 std::string hole_loc = it.first;
 357                                 std::string hole_value = it.second;
 358
 359                                 auto pos = hole_loc_to_name.find(hole_loc);
 360                                 log_assert(pos != hole_loc_to_name.end());
 361
 362                                 std::string hole_name = hole_loc_to_name[hole_loc];
 363                                 RTLIL::Wire *wire = module->wire(hole_name);
 364                                 log_assert(wire != nullptr);
 365
 366                                 log("Specializing %s with %s = %s.\n", module->name.c_str(), hole_name.c_str(), hole_value.c_str());
 367                                 module->connect(wire, hole_value);
 368                         }
 369                         Pass::call(design, "opt_clean");
 370                 }
 371         }
 372 } QbfSatPass;
 373
 374 PRIVATE_NAMESPACE_END