From aea0fd5ed4f5f56b81c43fe410efced194ef6472 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Sat, 25 Apr 2020 04:12:02 +0000 Subject: [PATCH] qbfsat: Add bisection mode and make it the default. Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit. --- passes/sat/qbfsat.cc | 294 ++++++++++++++++++++++++++++++------------- 1 file changed, 207 insertions(+), 87 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index d99ca1b53..0484b57b3 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -19,6 +19,7 @@ #include "kernel/yosys.h" #include "kernel/celltypes.h" +#include "kernel/consteval.h" #include "kernel/log.h" #include "kernel/rtlil.h" #include "kernel/register.h" @@ -43,13 +44,13 @@ struct QbfSolutionType { dict hole_to_value; bool sat; bool unknown; //true if neither 'sat' nor 'unsat' - bool success; //true if exit code 0 - QbfSolutionType() : sat(false), unknown(true), success(false) {} + QbfSolutionType() : sat(false), unknown(true) {} }; struct QbfSolveOptions { bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg; + bool nooptimize, nobisection; bool sat, unsat, show_smtbmc; std::string specialize_soln_file; std::string write_soln_soln_file; @@ -57,12 +58,14 @@ struct QbfSolveOptions { size_t argidx; QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false), - sat(false), unsat(false), show_smtbmc(false), argidx(0) {}; + nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false), + argidx(0) {}; }; void recover_solution(QbfSolutionType &sol) { YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); + YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\""); YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); #ifndef NDEBUG YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); @@ -86,6 +89,10 @@ void recover_solution(QbfSolutionType &sol) { sat_regex_found = true; else if (YS_REGEX_NS::regex_search(x, unsat_regex)) unsat_regex_found = true; + else if (YS_REGEX_NS::regex_search(x, memout_regex)) { + sol.unknown = true; + log_warning("solver ran out of memory\n"); + } } #ifndef NDEBUG log_assert(!sol.unknown && sol.sat? sat_regex_found : true); @@ -107,6 +114,40 @@ dict get_hole_loc_name_map(RTLIL::Module *module, cons return hole_loc_to_name; } +pool validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { + bool found_input = false; + bool found_hole = false; + bool found_1bit_output = false; + bool found_assert_assume = false; + pool input_wires; + for (auto wire : module->wires()) { + if (wire->port_input) { + found_input = true; + input_wires.insert(wire->name.str()); + } + if (wire->port_output && wire->width == 1) + found_1bit_output = true; + } + for (auto cell : module->cells()) { + if (cell->type == "$allconst") + found_input = true; + if (cell->type == "$anyconst") + found_hole = true; + if (cell->type.in("$assert", "$assume")) + found_assert_assume = true; + } + if (!found_input) + log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n"); + if (!found_hole) + log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); + if (!found_1bit_output && !found_assert_assume) + log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); + if (!found_assert_assume && !opt.assume_outputs) + log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n"); + + return input_wires; +} + void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) { std::ofstream fout(file.c_str()); if (!fout) @@ -164,7 +205,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { } } -void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { +void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) { dict hole_loc_to_name = get_hole_loc_name_map(module, sol); pool anyconsts_to_remove; for (auto cell : module->cells()) @@ -189,7 +230,8 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { log_assert(wire->width > 0 && GetSize(hole_value) == wire->width); #endif - log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); + if (!quiet) + log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); std::vector value_bv; value_bv.reserve(wire->width); for (char c : hole_value) @@ -219,7 +261,6 @@ void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); std::reverse(value_bv.begin(), value_bv.end()); } - } void allconstify_inputs(RTLIL::Module *module, const pool &input_wires) { @@ -280,84 +321,153 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1); } -QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { +QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, const std::string &tempdir_name, const bool quiet = false, const int iter_num = 0) { + //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 ]` QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; + const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2"; + 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"; const std::string smtbmc_warning = "z3: WARNING:"; const bool show_smtbmc = opt.show_smtbmc; - const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX"); - const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2"; -#ifndef NDEBUG - log_assert(mod->design != nullptr); -#endif Pass::call(mod->design, smt2_command); - log_header(mod->design, "Solving QBF-SAT problem.\n"); - //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 ]` - { - const std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1"; - auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](const std::string &line) { - ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline - auto warning_pos = line.find(smtbmc_warning); - if (warning_pos != std::string::npos) - log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); - else - if (show_smtbmc) - log("smtbmc output: %s", line.c_str()); - }; - - log("Launching \"%s\".\n", cmd.c_str()); - int retval = run_command(cmd, process_line); - if (retval == 0) { - ret.sat = true; - ret.unknown = false; - } else if (retval == 1) { - ret.sat = false; - ret.unknown = false; - } + auto process_line = [&ret, &smtbmc_warning, &show_smtbmc, &quiet](const std::string &line) { + ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline + auto warning_pos = line.find(smtbmc_warning); + if (warning_pos != std::string::npos) + log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); + else + if (show_smtbmc && !quiet) + log("smtbmc output: %s", line.c_str()); + }; + log_header(mod->design, "Solving QBF-SAT problem.\n"); + if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str()); + int retval = run_command(smtbmc_cmd, process_line); + if (retval == 0) { + ret.sat = true; + ret.unknown = false; + } else if (retval == 1) { + ret.sat = false; + ret.unknown = false; } - if(!opt.nocleanup) - remove_directory(tempdir_name); - recover_solution(ret); - return ret; } -pool validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { - bool found_input = false; - bool found_hole = false; - bool found_1bit_output = false; - bool found_assert_assume = false; - pool input_wires; - for (auto wire : module->wires()) { - if (wire->port_input) { - found_input = true; - input_wires.insert(wire->name.str()); - } - if (wire->port_output && wire->width == 1) - found_1bit_output = true; +QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { + QbfSolutionType ret, best_soln; + const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX"); + RTLIL::Module *module = mod; + RTLIL::Design *design = module->design; + std::string module_name = module->name.str(); + RTLIL::Wire *wire_to_optimize = nullptr; + RTLIL::IdString wire_to_optimize_name; + bool maximize = false; + log_assert(module->design != nullptr); + + Pass::call(design, "design -push-copy"); + + //Replace input wires with wires assigned $allconst cells: + pool input_wires = validate_design_and_get_inputs(module, opt); + allconstify_inputs(module, input_wires); + if (opt.assume_outputs) + assume_miter_outputs(module, opt); + + //Find the wire to be optimized, if any: + for (auto wire : module->wires()) + if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) + wire_to_optimize = wire; + if (wire_to_optimize != nullptr) { + wire_to_optimize_name = wire_to_optimize->name; + maximize = wire_to_optimize->get_bool_attribute("\\maximize"); } - for (auto cell : module->cells()) { - if (cell->type == "$allconst") - found_input = true; - if (cell->type == "$anyconst") - found_hole = true; - if (cell->type.in("$assert", "$assume")) - found_assert_assume = true; + + if (opt.nobisection || opt.nooptimize) { + if (wire_to_optimize != nullptr && opt.nooptimize) { + wire_to_optimize->set_bool_attribute("\\maximize", false); + wire_to_optimize->set_bool_attribute("\\minimize", false); + } + ret = call_qbf_solver(module, opt, tempdir_name, false, 0); + } else { + //Do the iterated bisection method: + unsigned int iter_num = 1; + unsigned int success = 0; + unsigned int failure = 0; + unsigned int cur_thresh = 0; + + log_assert(wire_to_optimize != nullptr); + log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize)); + + //If maximizing, grow until we get a failure. Then bisect success and failure. + while (failure == 0 || success - failure > 1) { + Pass::call(design, "design -push-copy"); + log_header(design, "Preparing QBF-SAT problem.\n"); + + if (cur_thresh != 0) { + //Add thresholding logic (but not on the initial run when we don't have a sense of where to start): + RTLIL::SigSpec comparator = maximize? module->Ge(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false) + : module->Le(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false); + + module->addAssume(wire_to_optimize_name.str() + "__threshold", comparator, RTLIL::Const(1, 1)); + log("Trying to solve with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), cur_thresh); + } + + ret = call_qbf_solver(module, opt, tempdir_name, false, iter_num); + Pass::call(design, "design -pop"); + module = design->module(module_name); + + if (!ret.unknown && ret.sat) { + Pass::call(design, "design -push-copy"); + specialize(module, ret, true); + + RTLIL::SigSpec wire, value, undef; + RTLIL::SigSpec::parse_sel(wire, design, module, wire_to_optimize_name.str()); + + ConstEval ce(module); + value = wire; + if (!ce.eval(value, undef)) + log_cmd_error("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(wire), log_signal(undef)); + log_assert(value.is_fully_const()); + success = value.as_const().as_int(); + best_soln = ret; + log("Problem is satisfiable with %s = %d.\n", wire_to_optimize_name.c_str(), success); + Pass::call(design, "design -pop"); + module = design->module(module_name); + + //sometimes this happens if we get an 'unknown' or timeout + if (!maximize && success < failure) + break; + else if (maximize && success > failure) + break; + } else { + //Treat 'unknown' as UNSAT + failure = cur_thresh; + if (failure == 0) { + log("Problem is NOT satisfiable.\n"); + break; + } + else + log("Problem is NOT satisfiable with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), failure); + } + + iter_num++; + cur_thresh = (maximize && failure == 0)? 2 * success //growth + : (success + failure) / 2; //bisection + } + if (success != 0 || failure != 0) { + log("Wire %s is %s at %d.\n", wire_to_optimize_name.c_str(), (maximize? "maximized" : "minimized"), success); + ret = best_soln; + } } - if (!found_input) - log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n"); - if (!found_hole) - log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); - if (!found_1bit_output && !found_assert_assume) - log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); - if (!found_assert_assume && !opt.assume_outputs) - log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n"); - return input_wires; + if(!opt.nocleanup) + remove_directory(tempdir_name); + + Pass::call(design, "design -pop"); + + return ret; } QbfSolveOptions parse_args(const std::vector &args) { @@ -379,6 +489,14 @@ QbfSolveOptions parse_args(const std::vector &args) { opt.assume_neg = true; continue; } + else if (args[opt.argidx] == "-nooptimize") { + opt.nooptimize = true; + continue; + } + else if (args[opt.argidx] == "-nobisection") { + opt.nobisection = true; + continue; + } else if (args[opt.argidx] == "-sat") { opt.sat = true; continue; @@ -477,6 +595,17 @@ struct QbfSatPass : public Pass { log(" negative polarity signals and should always be low, for example like the\n"); log(" miters created with the `miter` command.\n"); log("\n"); + log(" -nooptimize\n"); + log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n"); + log(" \"(minimize)\" in the SMTLIBv2, and generally make no attempt to optimize anything.\n"); + log("\n"); + log(" -nobisection\n"); + log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n"); + log(" attempt to optimize that value with the default iterated solving and threshold\n"); + log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n"); + log(" command in the SMTLIBv2 output and hope that the solver supports optimizing\n"); + log(" quantified bitvector problems.\n"); + log("\n"); log(" -sat\n"); log(" Generate an error if the solver does not return \"sat\".\n"); log("\n"); @@ -519,26 +648,16 @@ struct QbfSatPass : public Pass { if (!opt.specialize_from_file) { //Save the design to restore after modiyfing the current module. std::string module_name = module->name.str(); - Pass::call(design, "design -push-copy"); - - //Replace input wires with wires assigned $allconst cells. - pool input_wires = validate_design_and_get_inputs(module, opt); - allconstify_inputs(module, input_wires); - if (opt.assume_outputs) - assume_miter_outputs(module, opt); QbfSolutionType ret = qbf_solve(module, opt); - Pass::call(design, "design -pop"); module = design->module(module_name); - - if (ret.unknown) + if (ret.unknown) { log_warning("solver did not give an answer\n"); - else if (ret.sat) + if (opt.sat || opt.unsat) + log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); + } + else if (ret.sat) { print_qed(); - else - print_proof_failed(); - - if(!ret.unknown && ret.sat) { if (opt.write_solution) { write_solution(module, ret, opt.write_soln_soln_file); } @@ -550,10 +669,11 @@ struct QbfSatPass : public Pass { if (opt.unsat) log_cmd_error("expected problem to be UNSAT\n"); } - else if (!ret.unknown && !ret.sat && opt.sat) - log_cmd_error("expected problem to be SAT\n"); - else if (ret.unknown && (opt.sat || opt.unsat)) - log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); + else { + print_proof_failed(); + if (opt.sat) + log_cmd_error("expected problem to be SAT\n"); + } } else specialize_from_file(module, opt.specialize_soln_file); log_pop(); -- 2.30.2