mirror of https://github.com/YosysHQ/yosys.git
qbfsat: Add bisection mode and make it the default.
Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit.
This commit is contained in:
Alberto Gonzalez
parent
283b1130a6
commit
aea0fd5ed4
|
|
@ -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,86 +321,155 @@ 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);
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
//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());
|
||||
};
|
||||
recover_solution(ret);
|
||||
return ret;
|
||||
}
|
||||
|
||||
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;
|
||||
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");
|
||||
}
|
||||
|
||||
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(!opt.nocleanup)
|
||||
remove_directory(tempdir_name);
|
||||
|
||||
recover_solution(ret);
|
||||
Pass::call(design, "design -pop");
|
||||
|
||||
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;
|
||||
}
|
||||
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;
|
||||
}
|
||||
|
||||
QbfSolveOptions parse_args(const std::vector<std::string> &args) {
|
||||
QbfSolveOptions opt;
|
||||
for (opt.argidx = 1; opt.argidx < args.size(); opt.argidx++) {
|
||||
|
|
@ -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();
|
||||
|
|
|
|||
Loading…
Reference in New Issue