riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #2138 from boqwxp/qbfsat-oflag 

qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC
This commit is contained in:
clairexen 2020-07-01 16:35:27 +02:00 committed by GitHub
parent 2b0f6e24e2 83c595aaac
commit b1707407a0
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 47 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
passes/sat/qbfsat.cc
View File

@ -51,6 +51,7 @@ struct QbfSolveOptions {
bool nooptimize, nobisection; bool nooptimize, nobisection;
bool sat, unsat, show_smtbmc; bool sat, unsat, show_smtbmc;
enum Solver{Z3, Yices, CVC4} solver; enum Solver{Z3, Yices, CVC4} solver;
enum OptimizationLevel{O0, O1, O2} oflag;
int timeout; int timeout;
std::string specialize_soln_file; std::string specialize_soln_file;
std::string write_soln_soln_file; std::string write_soln_soln_file;
@ -59,7 +60,7 @@ struct QbfSolveOptions {
QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false), nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false), nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
solver(Yices), timeout(0), argidx(0) {}; solver(Yices), oflag(O0), timeout(0), argidx(0) {};
}; };
std::string get_solver_name(const QbfSolveOptions &opt) { std::string get_solver_name(const QbfSolveOptions &opt) {
@ -460,8 +461,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
RTLIL::Module *module = mod; RTLIL::Module *module = mod;
RTLIL::Design *design = module->design; RTLIL::Design *design = module->design;
std::string module_name = module->name.str(); std::string module_name = module->name.str();
RTLIL::Wire *wire_to_optimize = nullptr; RTLIL::IdString wire_to_optimize_name = "";
RTLIL::IdString wire_to_optimize_name;
bool maximize = false; bool maximize = false;
log_assert(module->design != nullptr); log_assert(module->design != nullptr);
@ -474,19 +474,30 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
assume_miter_outputs(module, opt); assume_miter_outputs(module, opt);
//Find the wire to be optimized, if any: //Find the wire to be optimized, if any:
for (auto wire : module->wires()) for (auto wire : module->wires()) {
if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) {
wire_to_optimize = wire; wire_to_optimize_name = wire->name;
if (wire_to_optimize != nullptr) { maximize = wire->get_bool_attribute("\\maximize");
wire_to_optimize_name = wire_to_optimize->name; if (opt.nooptimize) {
maximize = wire_to_optimize->get_bool_attribute("\\maximize"); if (maximize)
wire->set_bool_attribute("\\maximize", false);
else
wire->set_bool_attribute("\\minimize", false);
}
}
} }
if (opt.nobisection || opt.nooptimize || wire_to_optimize == nullptr) { //If -O1 or -O2 was specified, use ABC to simplify the problem:
if (wire_to_optimize != nullptr && opt.nooptimize) { if (opt.oflag == opt.OptimizationLevel::O1)
wire_to_optimize->set_bool_attribute("\\maximize", false); Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;fraig;print_stats;refactor,-N,10,-lz;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str());
wire_to_optimize->set_bool_attribute("\\minimize", false); else if (opt.oflag == opt.OptimizationLevel::O2)
} Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;dch,-S,1000000,-C,100000,-p;print_stats;fraig;print_stats;refactor,-N,15,-lz;print_stats;dc2,-pbl;print_stats;drwsat;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str());
if (opt.oflag != opt.OptimizationLevel::O0) {
Pass::call(module->design, "techmap");
Pass::call(module->design, "opt");
}
if (opt.nobisection || opt.nooptimize || wire_to_optimize_name == "") {
ret = call_qbf_solver(module, opt, tempdir_name, false, 0); ret = call_qbf_solver(module, opt, tempdir_name, false, 0);
} else { } else {
//Do the iterated bisection method: //Do the iterated bisection method:
@ -495,8 +506,9 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
unsigned int failure = 0; unsigned int failure = 0;
unsigned int cur_thresh = 0; unsigned int cur_thresh = 0;
log_assert(wire_to_optimize != nullptr); log_assert(wire_to_optimize_name != "");
log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize)); log_assert(module->wire(wire_to_optimize_name) != nullptr);
log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), wire_to_optimize_name.c_str());
//If maximizing, grow until we get a failure. Then bisect success and failure. //If maximizing, grow until we get a failure. Then bisect success and failure.
while (failure == 0 || difference(success, failure) > 1) { while (failure == 0 || difference(success, failure) > 1) {
@ -629,6 +641,22 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
} }
continue; continue;
} }
else if (args[opt.argidx].substr(0, 2) == "-O" && args[opt.argidx].size() == 3) {
switch (args[opt.argidx][2]) {
case '0':
opt.oflag = opt.OptimizationLevel::O0;
break;
case '1':
opt.oflag = opt.OptimizationLevel::O1;
break;
case '2':
opt.oflag = opt.OptimizationLevel::O2;
break;
default:
log_cmd_error("unknown argument %s\n", args[opt.argidx].c_str());
}
continue;
}
else if (args[opt.argidx] == "-sat") { else if (args[opt.argidx] == "-sat") {
opt.sat = true; opt.sat = true;
continue; continue;
@ -743,6 +771,9 @@ struct QbfSatPass : public Pass {
log(" -timeout <value>\n"); log(" -timeout <value>\n");
log(" Set the per-iteration timeout in seconds.\n"); log(" Set the per-iteration timeout in seconds.\n");
log("\n"); log("\n");
log(" -O0, -O1, -O2\n");
log(" Control the use of ABC to simplify the QBF-SAT problem before solving.\n");
log("\n");
log(" -sat\n"); log(" -sat\n");
log(" Generate an error if the solver does not return \"sat\".\n"); log(" Generate an error if the solver does not return \"sat\".\n");
log("\n"); log("\n");