From aea0fd5ed4f5f56b81c43fe410efced194ef6472 Mon Sep 17 00:00:00 2001
From: Alberto Gonzalez <boqwxp@airmail.cc>
Date: Sat, 25 Apr 2020 04:12:02 +0000
Subject: 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(-)
(limited to 'passes/sat/qbfsat.cc')
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<std::string, std::string> 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<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, cons
return hole_loc_to_name;
}
+pool<std::string> 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<std::string> 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<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
pool<RTLIL::Cell *> 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<RTLIL::SigBit> 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<std::string> &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 <file>]`
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 <file>]`
- {
- 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<std::string> 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<std::string> 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<std::string> 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<std::string> &args) {
@@ -379,6 +489,14 @@ QbfSolveOptions parse_args(const std::vector<std::string> &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<std::string> 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();
--
cgit v1.2.3