From fb878b2a70c8e8e8201a3b4581a07839d7c1261c Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Mon, 23 Mar 2020 07:42:48 +0000 Subject: [PATCH 01/24] Initial skeleton for `qbfsat` command. --- passes/sat/Makefile.inc | 1 + passes/sat/qbfsat.cc | 206 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 207 insertions(+) create mode 100644 passes/sat/qbfsat.cc diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index 4bb4b0edc..a928c57de 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -13,4 +13,5 @@ OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o OBJS += passes/sat/cutpoint.o OBJS += passes/sat/fminit.o +OBJS += passes/sat/qbfsat.o diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc new file mode 100644 index 000000000..5418256bc --- /dev/null +++ b/passes/sat/qbfsat.cc @@ -0,0 +1,206 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2020 Alberto Gonzalez + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/register.h" +#include "kernel/celltypes.h" +#include "kernel/log.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct QbfSolutionType { + std::vector stdout; + 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 qbf_solve(RTLIL::Module *mod) { + + QbfSolutionType ret; + + //TODO: make temporary directory + //TODO: call `prep` + //TODO: call `write_smt2` + //TODO: execute and capture stdout from `yosys-smtbmc` + //TODO: remove temporary directory + + return ret; +} + +void print_proof_failed() +{ + log("\n"); + log(" ______ ___ ___ _ _ _ _ \n"); + log(" (_____ \\ / __) / __) (_) | | | |\n"); + log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n"); + log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n"); + log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n"); + log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n"); + log("\n"); +} + +void print_timeout() +{ + log("\n"); + log(" _____ _ _ _____ ____ _ _____\n"); + log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n"); + log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n"); + log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n"); + log(" \\_/ \\_/\\_/ \\|\\____\\\\____/\\____/ \\_/\n"); + log("\n"); +} + +void print_qed() +{ + log("\n"); + log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n"); + log(" /$$__ $$ | $$_____/ | $$__ $$ \n"); + log(" | $$ \\ $$ | $$ | $$ \\ $$ \n"); + log(" | $$ | $$ | $$$$$ | $$ | $$ \n"); + log(" | $$ | $$ | $$__/ | $$ | $$ \n"); + log(" | $$/$$ $$ | $$ | $$ | $$ \n"); + log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n"); + log(" \\____ $$$|__/|________/|__/|_______/|__/\n"); + log(" \\__/ \n"); + log("\n"); +} + +struct QbfSatPass : public Pass { + QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { } + void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" qbfsat [options] [selection]\n"); + log("\n"); + log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n"); + log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n"); + log("Universally-quantified variables may be explicitly declared by assigning a wire\n"); + log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n"); + log("by default.\n"); + log("\n"); + log(" -timeout \n"); + log(" Set the solver timeout to the specified number of seconds.\n"); + log("\n"); + log(" -specialize\n"); + log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n"); + log("\n"); + log(" -specialize-from-file \n"); + log(" Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n"); + log(" cells in the current module with values provided by the specified file.\n"); + log("\n"); + log(" -write-solution \n"); + log(" Write the assignments discovered by the solver for all \"$anyconst\" cells\n"); + log(" to the specified file."); + log("\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE + { + bool timeout = false, specialize = false, specialize_from_file = false, write_solution = false; + long timeout_sec = -1; + std::string specialize_soln_file; + std::string write_soln_soln_file; + + log_header(design, "Executing QBF-SAT pass (solving QBF-SAT problems in the circuit).\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-timeout") { + timeout = true; + if (args.size() <= argidx + 1) + log_cmd_error("timeout not specified.\n"); + else + timeout_sec = atol(args[++argidx].c_str()); + continue; + } + else if (args[argidx] == "-specialize") { + specialize = true; + continue; + } + else if (args[argidx] == "-specialize-from-file") { + specialize_from_file = true; + if (args.size() <= argidx + 1) + log_cmd_error("solution file not specified.\n"); + else + specialize_soln_file = args[++argidx]; + continue; + } + else if (args[argidx] == "-write-solution") { + write_solution = true; + if (args.size() <= argidx + 1) + log_cmd_error("solution file not specified.\n"); + else + write_soln_soln_file = args[++argidx]; + continue; + } + break; + } + extra_args(args, argidx, design); + + RTLIL::Module *module = NULL; + for (auto mod : design->selected_modules()) { + if (module) + 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)); + module = mod; + } + if (module == NULL) + log_cmd_error("Can't perform QBF-SAT on an empty selection!\n"); + + bool found_input = false; + bool found_hole = false; + bool found_1bit_output = false; + for (auto wire : module->wires()) { + if (wire->port_input) + found_input = true; + 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_1bit_output = 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) + log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n"); + + QbfSolutionType ret = qbf_solve(module); + + if (ret.unknown) + log_warning("solver did not give an answer\n"); + else if (ret.sat) + print_qed(); + else + print_proof_failed(); + + //TODO specialize etc. + } +} QbfSatPass; + +PRIVATE_NAMESPACE_END From 2fff574741ae0af47c8665636347d0a0d3cef5e6 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 01:58:41 +0000 Subject: [PATCH 02/24] Barebones implementation of `qbfsat` command. --- passes/sat/qbfsat.cc | 189 +++++++++++++++++++++++++++++++++++-------- 1 file changed, 157 insertions(+), 32 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 5418256bc..dd57b91c9 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -17,9 +17,22 @@ * */ -#include "kernel/register.h" +#include "kernel/yosys.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include "kernel/rtlil.h" +#include "kernel/register.h" +#include + +#if defined(_WIN32) +# define WIFEXITED(x) 1 +# define WIFSIGNALED(x) 0 +# define WIFSTOPPED(x) 0 +# define WEXITSTATUS(x) ((x) & 0xff) +# define WTERMSIG(x) SIGTERM +#else +# include +#endif USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -33,16 +46,100 @@ struct QbfSolutionType { QbfSolutionType() : sat(false), unknown(true), success(false) {} }; -QbfSolutionType qbf_solve(RTLIL::Module *mod) { +struct QbfSolveOptions { + bool timeout, specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2; + long timeout_sec; + std::string specialize_soln_file; + std::string write_soln_soln_file; + std::string dump_final_smt2_file; + QbfSolveOptions() : timeout(false), specialize(false), specialize_from_file(false), write_solution(false), + nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {}; +}; + +QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; + std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; + std::string smtbmc_warning = "z3: WARNING:"; - //TODO: make temporary directory - //TODO: call `prep` - //TODO: call `write_smt2` - //TODO: execute and capture stdout from `yosys-smtbmc` - //TODO: remove temporary directory + std::string tempdir_name = "/tmp/yosys-z3-XXXXXX"; + tempdir_name = make_temp_dir(tempdir_name); + std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2"; + log_assert(mod->design != nullptr); + Pass::call(mod->design, smt2_command); + //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g [--dump-smt2 ]` + { + fflush(stdout); + bool keep_reading = true; + int status = 0; + int retval = 0; + char buf[1024] = {0}; + std::string linebuf = ""; + 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"; + log("Launching \"%s\".\n", cmd.c_str()); + +#ifndef EMSCRIPTEN + FILE *f = popen(cmd.c_str(), "r"); + if (f == nullptr) + log_cmd_error("errno %d after popen() returned NULL.\n", errno); + while (keep_reading) { + keep_reading = (fgets(buf, sizeof(buf), f) != nullptr); + linebuf += buf; + memset(buf, 0, sizeof(buf)); + + auto pos = linebuf.find('\n'); + while (pos != std::string::npos) { + std::string line = linebuf.substr(0, pos); + linebuf.erase(0, pos + 1); + ret.stdout.push_back(line); + auto warning_pos = line.find(smtbmc_warning); + if(warning_pos != std::string::npos) + log_warning("%s\n", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); + else + log("smtbmc output: %s\n", line.c_str()); + + pos = linebuf.find('\n'); + } + } + status = pclose(f); +#endif + + if(WIFEXITED(status)) { + retval = WEXITSTATUS(status); + } + else if(WIFSIGNALED(status)) { + retval = WTERMSIG(status); + } + else if(WIFSTOPPED(status)) { + retval = WSTOPSIG(status); + } + + 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); + + YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); + bool sat_regex_found = false; + YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); + bool unsat_regex_found = false; + for (auto &x : ret.stdout) { + //TODO: recover values here for later specialization? + if (YS_REGEX_NS::regex_search(x, sat_regex)) + sat_regex_found = true; + if (YS_REGEX_NS::regex_search(x, unsat_regex)) + unsat_regex_found = true; + } + log_assert(ret.sat? sat_regex_found : true); + log_assert(!ret.unknown && !ret.sat? unsat_regex_found : true); return ret; } @@ -58,17 +155,6 @@ void print_proof_failed() log("\n"); } -void print_timeout() -{ - log("\n"); - log(" _____ _ _ _____ ____ _ _____\n"); - log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n"); - log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n"); - log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n"); - log(" \\_/ \\_/\\_/ \\|\\____\\\\____/\\____/ \\_/\n"); - log("\n"); -} - void print_qed() { log("\n"); @@ -101,6 +187,13 @@ struct QbfSatPass : public Pass { log(" -timeout \n"); log(" Set the solver timeout to the specified number of seconds.\n"); log("\n"); + log(" -nocleanup\n"); + log(" Do not delete temporary files and directories. Useful for\n"); + log(" debugging.\n"); + log("\n"); + log(" -dump-final-smt2 \n"); + log(" Pass the --dump-smt2 option to yosys-smtbmc.\n"); + log("\n"); log(" -specialize\n"); log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n"); log("\n"); @@ -116,41 +209,49 @@ struct QbfSatPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE { - bool timeout = false, specialize = false, specialize_from_file = false, write_solution = false; - long timeout_sec = -1; - std::string specialize_soln_file; - std::string write_soln_soln_file; - + QbfSolveOptions opt; log_header(design, "Executing QBF-SAT pass (solving QBF-SAT problems in the circuit).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { if (args[argidx] == "-timeout") { - timeout = true; + opt.timeout = true; if (args.size() <= argidx + 1) log_cmd_error("timeout not specified.\n"); else - timeout_sec = atol(args[++argidx].c_str()); + opt.timeout_sec = atol(args[++argidx].c_str()); + continue; + } + else if (args[argidx] == "-nocleanup") { + opt.nocleanup = true; continue; } else if (args[argidx] == "-specialize") { - specialize = true; + opt.specialize = true; + continue; + } + else if (args[argidx] == "-dump-final-smt2") { + opt.dump_final_smt2 = true; + if (args.size() <= argidx + 1) + log_cmd_error("smt2 file not specified.\n"); + else + opt.dump_final_smt2_file = args[++argidx]; continue; } else if (args[argidx] == "-specialize-from-file") { - specialize_from_file = true; + opt.specialize_from_file = true; if (args.size() <= argidx + 1) log_cmd_error("solution file not specified.\n"); else - specialize_soln_file = args[++argidx]; + opt.specialize_soln_file = args[++argidx]; continue; } else if (args[argidx] == "-write-solution") { - write_solution = true; + opt.write_solution = true; if (args.size() <= argidx + 1) log_cmd_error("solution file not specified.\n"); else - write_soln_soln_file = args[++argidx]; + opt.write_soln_soln_file = args[++argidx]; continue; } break; @@ -169,9 +270,12 @@ struct QbfSatPass : public Pass { bool found_input = false; bool found_hole = false; bool found_1bit_output = false; + std::set input_wires; for (auto wire : module->wires()) { - if (wire->port_input) + if (wire->port_input) { found_input = true; + input_wires.insert(wire->name.str()); + } if (wire->port_output && wire->width == 1) found_1bit_output = true; } @@ -190,7 +294,26 @@ struct QbfSatPass : public Pass { if (!found_1bit_output) log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n"); - QbfSolutionType ret = qbf_solve(module); + //Do not modify the current design. Operate on a clone of the selected module. + RTLIL::Design *new_design = new Design(); + module = module->clone(); + new_design->add(module); + + //Replace input wires with wires assigned $allconst cells. + for(auto &n : input_wires) { + RTLIL::Wire *input = module->wire(n); + log_assert(input != nullptr); + + RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst"); + allconst->setParam(ID(WIDTH), input->width); + allconst->setPort(ID::Y, input); + allconst->set_src_attribute(input->get_src_attribute()); + input->port_input = false; + log("Replaced input %s with $allconst cell.\n", n.c_str()); + } + module->fixup_ports(); + + QbfSolutionType ret = qbf_solve(module, opt); if (ret.unknown) log_warning("solver did not give an answer\n"); @@ -200,6 +323,8 @@ struct QbfSatPass : public Pass { print_proof_failed(); //TODO specialize etc. + + delete new_design; } } QbfSatPass; From a4598d64ef5f8386b28019bb64b7ad2d6e0c9d7e Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 22:37:54 +0000 Subject: [PATCH 03/24] Hole value recovery and specialization implementation for `qbfsat` command. --- kernel/log.h | 7 ++++ passes/sat/qbfsat.cc | 83 +++++++++++++++++++++++++++++++++----------- 2 files changed, 70 insertions(+), 20 deletions(-) diff --git a/kernel/log.h b/kernel/log.h index cd0e8185c..5478482ac 100644 --- a/kernel/log.h +++ b/kernel/log.h @@ -29,18 +29,25 @@ #if defined(__GNUC__) && !defined( __clang__) && ( __GNUC__ == 4 && __GNUC_MINOR__ <= 8) #include #define YS_REGEX_TYPE boost::xpressive::sregex + #define YS_REGEX_MATCH_TYPE boost::xpressive::smatch #define YS_REGEX_NS boost::xpressive #define YS_REGEX_COMPILE(param) boost::xpressive::sregex::compile(param, \ boost::xpressive::regex_constants::nosubs | \ boost::xpressive::regex_constants::optimize) + #define YS_REGEX_COMPILE_WITH_SUBS(param) boost::xpressive::sregex::compile(param, \ + boost::xpressive::regex_constants::optimize) # else #include #define YS_REGEX_TYPE std::regex + #define YS_REGEX_MATCH_TYPE std::smatch #define YS_REGEX_NS std #define YS_REGEX_COMPILE(param) std::regex(param, \ std::regex_constants::nosubs | \ std::regex_constants::optimize | \ std::regex_constants::egrep) + #define YS_REGEX_COMPILE_WITH_SUBS(param) std::regex(param, \ + std::regex_constants::optimize | \ + std::regex_constants::egrep) #endif #ifndef _WIN32 diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index dd57b91c9..3045c2284 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -39,6 +39,7 @@ PRIVATE_NAMESPACE_BEGIN struct QbfSolutionType { std::vector stdout; + std::map hole_to_value; bool sat; bool unknown; //true if neither 'sat' nor 'unsat' bool success; //true if exit code 0 @@ -56,8 +57,34 @@ struct QbfSolveOptions { nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {}; }; -QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { +void recover_solution(RTLIL::Module *mod, 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 hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); + YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); + YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+"); + YS_REGEX_MATCH_TYPE m; + bool sat_regex_found = false; + bool unsat_regex_found = false; + std::map hole_value_recovered; + for (const std::string &x : sol.stdout) { + if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { + std::string loc = m[1].str(); + std::string val = m[2].str(); + log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex)); + log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex)); + sol.hole_to_value[loc] = val; + } + else if (YS_REGEX_NS::regex_search(x, sat_regex)) + sat_regex_found = true; + else if (YS_REGEX_NS::regex_search(x, unsat_regex)) + unsat_regex_found = true; + } + log_assert(!sol.unknown && sol.sat? sat_regex_found : true); + log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); +} +QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; std::string smtbmc_warning = "z3: WARNING:"; @@ -127,22 +154,12 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { if(!opt.nocleanup) remove_directory(tempdir_name); - YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); - bool sat_regex_found = false; - YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); - bool unsat_regex_found = false; - for (auto &x : ret.stdout) { - //TODO: recover values here for later specialization? - if (YS_REGEX_NS::regex_search(x, sat_regex)) - sat_regex_found = true; - if (YS_REGEX_NS::regex_search(x, unsat_regex)) - unsat_regex_found = true; - } - log_assert(ret.sat? sat_regex_found : true); - log_assert(!ret.unknown && !ret.sat? unsat_regex_found : true); + recover_solution(mod, ret); + return ret; } + void print_proof_failed() { log("\n"); @@ -294,10 +311,9 @@ struct QbfSatPass : public Pass { if (!found_1bit_output) log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n"); - //Do not modify the current design. Operate on a clone of the selected module. - RTLIL::Design *new_design = new Design(); - module = module->clone(); - new_design->add(module); + //Save the design to restore after modiyfing the current module. + std::string module_name = module->name.str(); + Pass::call(design, "design -save _qbfsat_tmp"); //Replace input wires with wires assigned $allconst cells. for(auto &n : input_wires) { @@ -314,6 +330,8 @@ struct QbfSatPass : public Pass { module->fixup_ports(); QbfSolutionType ret = qbf_solve(module, opt); + Pass::call(design, "design -load _qbfsat_tmp"); + module = design->module(module_name); if (ret.unknown) log_warning("solver did not give an answer\n"); @@ -322,9 +340,34 @@ struct QbfSatPass : public Pass { else print_proof_failed(); - //TODO specialize etc. + if (opt.specialize) { + std::map hole_loc_to_name; + for (auto cell : module->cells()) { + std::string cell_src = cell->get_src_attribute(); + auto pos = ret.hole_to_value.find(cell_src); + if (pos != ret.hole_to_value.end()) { + log_assert(cell->type.in("$anyconst", "$anyseq")); + log_assert(cell->hasPort(ID::Y)); + log_assert(cell->getPort(ID::Y).is_wire()); + hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); + } + } + for (auto &it : ret.hole_to_value) { + std::string hole_loc = it.first; + std::string hole_value = it.second; - delete new_design; + auto pos = hole_loc_to_name.find(hole_loc); + log_assert(pos != hole_loc_to_name.end()); + + std::string hole_name = hole_loc_to_name[hole_loc]; + RTLIL::Wire *wire = module->wire(hole_name); + log_assert(wire != nullptr); + + log("Specializing %s with %s = %s.\n", module->name.c_str(), hole_name.c_str(), hole_value.c_str()); + module->connect(wire, hole_value); + } + Pass::call(design, "opt_clean"); + } } } QbfSatPass; From 437afa1f0cbc6534dbb7ec9a4024276e75afce01 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 23:17:50 +0000 Subject: [PATCH 04/24] Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole value recovery using that mode. --- backends/smt2/smtbmc.py | 18 +++++++++-- passes/sat/qbfsat.cc | 68 +++++++++++++++++++++++------------------ 2 files changed, 54 insertions(+), 32 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 630464419..4af4c8ae0 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -49,6 +49,7 @@ presat = False smtcinit = False smtctop = None noinit = False +binarymode = False so = SmtOpts() @@ -150,6 +151,9 @@ yosys-smtbmc [options] add time steps at the end of the trace when creating a counter example (this additional time steps will still be constrained by assumptions) + + --binary + dump anyconst values as raw bit strings """ + so.helpmsg()) sys.exit(1) @@ -158,7 +162,7 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat", "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit"]) + "smtc-init", "smtc-top=", "noinit", "binary"]) except: usage() @@ -229,6 +233,8 @@ for o, a in opts: covermode = True elif o == "-m": topmod = a + elif o == "--binary": + binarymode = True elif so.handle(o, a): pass else: @@ -1089,9 +1095,15 @@ def print_anyconsts_worker(mod, state, path): for fun, info in smt.modinfo[mod].anyconsts.items(): if info[1] is None: - print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state))))) + if not binarymode: + print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state))))) + else: + print_msg("Value for anyconst in %s (%s): %s" % (path, info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state))))) else: - print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state))))) + if not binarymode: + print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state))))) + else: + print_msg("Value for anyconst %s.%s (%s): %s" % (path, info[1], info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state))))) def print_anyconsts(state): diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 3045c2284..cab6f53f3 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -23,6 +23,7 @@ #include "kernel/rtlil.h" #include "kernel/register.h" #include +#include #if defined(_WIN32) # define WIFEXITED(x) 1 @@ -57,7 +58,7 @@ struct QbfSolveOptions { nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {}; }; -void recover_solution(RTLIL::Module *mod, QbfSolutionType &sol) { +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 hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); @@ -84,6 +85,39 @@ void recover_solution(RTLIL::Module *mod, QbfSolutionType &sol) { log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); } +void specialize(RTLIL::Module *module, const QbfSolutionType &ret) { + std::map hole_loc_to_name; + for (auto cell : module->cells()) { + std::string cell_src = cell->get_src_attribute(); + auto pos = ret.hole_to_value.find(cell_src); + if (pos != ret.hole_to_value.end()) { + log_assert(cell->type.in("$anyconst", "$anyseq")); + log_assert(cell->hasPort(ID::Y)); + log_assert(cell->getPort(ID::Y).is_wire()); + hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); + } + } + for (auto &it : ret.hole_to_value) { + std::string hole_loc = it.first; + std::string hole_value = it.second; + + auto pos = hole_loc_to_name.find(hole_loc); + log_assert(pos != hole_loc_to_name.end()); + + std::string hole_name = hole_loc_to_name[hole_loc]; + RTLIL::Wire *wire = module->wire(hole_name); + log_assert(wire != nullptr); + + 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) + value_bv.push_back(c == '1'? RTLIL::S1 : RTLIL::S0); + std::reverse(value_bv.begin(), value_bv.end()); + module->connect(wire, value_bv); + } +} + QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; @@ -95,7 +129,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { log_assert(mod->design != nullptr); Pass::call(mod->design, smt2_command); - //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g [--dump-smt2 ]` + //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 ]` { fflush(stdout); bool keep_reading = true; @@ -103,7 +137,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { int retval = 0; char buf[1024] = {0}; std::string linebuf = ""; - 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"; + 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"; log("Launching \"%s\".\n", cmd.c_str()); #ifndef EMSCRIPTEN @@ -154,7 +188,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { if(!opt.nocleanup) remove_directory(tempdir_name); - recover_solution(mod, ret); + recover_solution(ret); return ret; } @@ -341,31 +375,7 @@ struct QbfSatPass : public Pass { print_proof_failed(); if (opt.specialize) { - std::map hole_loc_to_name; - for (auto cell : module->cells()) { - std::string cell_src = cell->get_src_attribute(); - auto pos = ret.hole_to_value.find(cell_src); - if (pos != ret.hole_to_value.end()) { - log_assert(cell->type.in("$anyconst", "$anyseq")); - log_assert(cell->hasPort(ID::Y)); - log_assert(cell->getPort(ID::Y).is_wire()); - hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); - } - } - for (auto &it : ret.hole_to_value) { - std::string hole_loc = it.first; - std::string hole_value = it.second; - - auto pos = hole_loc_to_name.find(hole_loc); - log_assert(pos != hole_loc_to_name.end()); - - std::string hole_name = hole_loc_to_name[hole_loc]; - RTLIL::Wire *wire = module->wire(hole_name); - log_assert(wire != nullptr); - - log("Specializing %s with %s = %s.\n", module->name.c_str(), hole_name.c_str(), hole_value.c_str()); - module->connect(wire, hole_value); - } + specialize(module, ret); Pass::call(design, "opt_clean"); } } From d07ac2612b144ad2486cff5e07f7e501da54e3f7 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 23:37:49 +0000 Subject: [PATCH 05/24] Clean up `passes/sat/qbfsat.cc`. --- passes/sat/qbfsat.cc | 187 +++++++++++++++++++++++-------------------- 1 file changed, 101 insertions(+), 86 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index cab6f53f3..b95c81501 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -54,8 +54,9 @@ struct QbfSolveOptions { std::string specialize_soln_file; std::string write_soln_soln_file; std::string dump_final_smt2_file; + size_t argidx; QbfSolveOptions() : timeout(false), specialize(false), specialize_from_file(false), write_solution(false), - nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {}; + nocleanup(false), dump_final_smt2(false), timeout_sec(-1), argidx(0) {}; }; void recover_solution(QbfSolutionType &sol) { @@ -118,6 +119,21 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &ret) { } } +void allconstify_inputs(RTLIL::Module *module, const std::set &input_wires) { + for(auto &n : input_wires) { + RTLIL::Wire *input = module->wire(n); + log_assert(input != nullptr); + + RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst"); + allconst->setParam(ID(WIDTH), input->width); + allconst->setPort(ID::Y, input); + allconst->set_src_attribute(input->get_src_attribute()); + input->port_input = false; + log("Replaced input %s with $allconst cell.\n", n.c_str()); + } + module->fixup_ports(); +} + QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; @@ -193,6 +209,86 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { return ret; } +std::set validate_design_and_get_inputs(RTLIL::Module *module) { + bool found_input = false; + bool found_hole = false; + bool found_1bit_output = false; + std::set 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_1bit_output = 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) + log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n"); + + return input_wires; +} + + +QbfSolveOptions parse_args(const std::vector &args) { + QbfSolveOptions opt; + for (opt.argidx = 1; opt.argidx < args.size(); opt.argidx++) { + if (args[opt.argidx] == "-timeout") { + opt.timeout = true; + if (args.size() <= opt.argidx + 1) + log_cmd_error("timeout not specified.\n"); + else + opt.timeout_sec = atol(args[++opt.argidx].c_str()); + continue; + } + else if (args[opt.argidx] == "-nocleanup") { + opt.nocleanup = true; + continue; + } + else if (args[opt.argidx] == "-specialize") { + opt.specialize = true; + continue; + } + else if (args[opt.argidx] == "-dump-final-smt2") { + opt.dump_final_smt2 = true; + if (args.size() <= opt.argidx + 1) + log_cmd_error("smt2 file not specified.\n"); + else + opt.dump_final_smt2_file = args[++opt.argidx]; + continue; + } + else if (args[opt.argidx] == "-specialize-from-file") { + opt.specialize_from_file = true; + if (args.size() <= opt.argidx + 1) + log_cmd_error("solution file not specified.\n"); + else + opt.specialize_soln_file = args[++opt.argidx]; + continue; + } + else if (args[opt.argidx] == "-write-solution") { + opt.write_solution = true; + if (args.size() <= opt.argidx + 1) + log_cmd_error("solution file not specified.\n"); + else + opt.write_soln_soln_file = args[++opt.argidx]; + continue; + } + break; + } + + return opt; +} void print_proof_failed() { @@ -260,54 +356,10 @@ struct QbfSatPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE { - QbfSolveOptions opt; log_header(design, "Executing QBF-SAT pass (solving QBF-SAT problems in the circuit).\n"); + QbfSolveOptions opt = parse_args(args); + extra_args(args, opt.argidx, design); - size_t argidx; - for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-timeout") { - opt.timeout = true; - if (args.size() <= argidx + 1) - log_cmd_error("timeout not specified.\n"); - else - opt.timeout_sec = atol(args[++argidx].c_str()); - continue; - } - else if (args[argidx] == "-nocleanup") { - opt.nocleanup = true; - continue; - } - else if (args[argidx] == "-specialize") { - opt.specialize = true; - continue; - } - else if (args[argidx] == "-dump-final-smt2") { - opt.dump_final_smt2 = true; - if (args.size() <= argidx + 1) - log_cmd_error("smt2 file not specified.\n"); - else - opt.dump_final_smt2_file = args[++argidx]; - continue; - } - else if (args[argidx] == "-specialize-from-file") { - opt.specialize_from_file = true; - if (args.size() <= argidx + 1) - log_cmd_error("solution file not specified.\n"); - else - opt.specialize_soln_file = args[++argidx]; - continue; - } - else if (args[argidx] == "-write-solution") { - opt.write_solution = true; - if (args.size() <= argidx + 1) - log_cmd_error("solution file not specified.\n"); - else - opt.write_soln_soln_file = args[++argidx]; - continue; - } - break; - } - extra_args(args, argidx, design); RTLIL::Module *module = NULL; for (auto mod : design->selected_modules()) { @@ -318,50 +370,13 @@ struct QbfSatPass : public Pass { if (module == NULL) log_cmd_error("Can't perform QBF-SAT on an empty selection!\n"); - bool found_input = false; - bool found_hole = false; - bool found_1bit_output = false; - std::set 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_1bit_output = 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) - log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n"); - //Save the design to restore after modiyfing the current module. std::string module_name = module->name.str(); Pass::call(design, "design -save _qbfsat_tmp"); //Replace input wires with wires assigned $allconst cells. - for(auto &n : input_wires) { - RTLIL::Wire *input = module->wire(n); - log_assert(input != nullptr); - - RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst"); - allconst->setParam(ID(WIDTH), input->width); - allconst->setPort(ID::Y, input); - allconst->set_src_attribute(input->get_src_attribute()); - input->port_input = false; - log("Replaced input %s with $allconst cell.\n", n.c_str()); - } - module->fixup_ports(); + std::set input_wires = validate_design_and_get_inputs(module); + allconstify_inputs(module, input_wires); QbfSolutionType ret = qbf_solve(module, opt); Pass::call(design, "design -load _qbfsat_tmp"); From b9e79e0bb76e0b45650005914ebf21c77e0242d1 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 23:51:32 +0000 Subject: [PATCH 06/24] Implement `-write-solution` option for the `qbfsat` command. --- passes/sat/qbfsat.cc | 35 ++++++++++++++++++++++++++++------- 1 file changed, 28 insertions(+), 7 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index b95c81501..6ac952ea4 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -86,19 +86,35 @@ void recover_solution(QbfSolutionType &sol) { log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); } -void specialize(RTLIL::Module *module, const QbfSolutionType &ret) { +std::map get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { std::map hole_loc_to_name; for (auto cell : module->cells()) { std::string cell_src = cell->get_src_attribute(); - auto pos = ret.hole_to_value.find(cell_src); - if (pos != ret.hole_to_value.end()) { + auto pos = sol.hole_to_value.find(cell_src); + if (pos != sol.hole_to_value.end()) { log_assert(cell->type.in("$anyconst", "$anyseq")); log_assert(cell->hasPort(ID::Y)); log_assert(cell->getPort(ID::Y).is_wire()); hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); } } - for (auto &it : ret.hole_to_value) { + + return hole_loc_to_name; +} + +void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) { + std::ofstream fout(file.c_str()); + if (!fout) + log_cmd_error("could not open solution file for writing.\n"); + + std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + for(auto &x : sol.hole_to_value) + fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl; +} + +void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { + std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + for (auto &it : sol.hole_to_value) { std::string hole_loc = it.first; std::string hole_value = it.second; @@ -389,9 +405,14 @@ struct QbfSatPass : public Pass { else print_proof_failed(); - if (opt.specialize) { - specialize(module, ret); - Pass::call(design, "opt_clean"); + if(!ret.unknown && ret.sat) { + if (opt.write_solution) { + write_solution(module, ret, opt.write_soln_soln_file); + } + if (opt.specialize) { + specialize(module, ret); + Pass::call(design, "opt_clean"); + } } } } QbfSatPass; From 3a4fd4a999771f54adb16bf2cc037c79e7e393e8 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Thu, 26 Mar 2020 01:02:53 +0000 Subject: [PATCH 07/24] Implement `-specialize-from-file` option for the `qbfsat` command. --- passes/sat/qbfsat.cc | 77 +++++++++++++++++++++++++++++++------------- 1 file changed, 55 insertions(+), 22 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 6ac952ea4..c301e9e94 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -112,6 +112,33 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl; } +void specialize_from_file(RTLIL::Module *module, const std::string &file) { + YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$"); + YS_REGEX_MATCH_TYPE m; + std::ifstream fin(file.c_str()); + if (!fin) + log_cmd_error("could not read solution file.\n"); + + std::string buf; + while (std::getline(fin, buf)) { + log_assert(YS_REGEX_NS::regex_search(buf, m, hole_assn_regex)); + std::string hole_name = m[1].str(); + std::string hole_value = m[2].str(); + + RTLIL::Wire *wire = module->wire(hole_name); + log_assert(wire != nullptr); + log_assert(wire->width > 0 && hole_value.size() == static_cast(wire->width)); + + log("Specializing %s from file 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) + value_bv.push_back(c == '1'? RTLIL::S1 : RTLIL::S0); + std::reverse(value_bv.begin(), value_bv.end()); + module->connect(wire, value_bv); + } +} + void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); for (auto &it : sol.hole_to_value) { @@ -124,6 +151,7 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { std::string hole_name = hole_loc_to_name[hole_loc]; RTLIL::Wire *wire = module->wire(hole_name); log_assert(wire != nullptr); + log_assert(wire->width > 0 && hole_value.size() == static_cast(wire->width)); 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; @@ -386,33 +414,38 @@ struct QbfSatPass : public Pass { if (module == NULL) log_cmd_error("Can't perform QBF-SAT on an empty selection!\n"); - //Save the design to restore after modiyfing the current module. - std::string module_name = module->name.str(); - Pass::call(design, "design -save _qbfsat_tmp"); + 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 -save _qbfsat_tmp"); - //Replace input wires with wires assigned $allconst cells. - std::set input_wires = validate_design_and_get_inputs(module); - allconstify_inputs(module, input_wires); + //Replace input wires with wires assigned $allconst cells. + std::set input_wires = validate_design_and_get_inputs(module); + allconstify_inputs(module, input_wires); - QbfSolutionType ret = qbf_solve(module, opt); - Pass::call(design, "design -load _qbfsat_tmp"); - module = design->module(module_name); + QbfSolutionType ret = qbf_solve(module, opt); + Pass::call(design, "design -load _qbfsat_tmp"); + module = design->module(module_name); - if (ret.unknown) - log_warning("solver did not give an answer\n"); - else if (ret.sat) - print_qed(); - else - print_proof_failed(); + if (ret.unknown) + log_warning("solver did not give an answer\n"); + 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); - } - if (opt.specialize) { - specialize(module, ret); - Pass::call(design, "opt_clean"); + if(!ret.unknown && ret.sat) { + if (opt.write_solution) { + write_solution(module, ret, opt.write_soln_soln_file); + } + if (opt.specialize) { + specialize(module, ret); + Pass::call(design, "opt_clean"); + } } + } else { + specialize_from_file(module, opt.specialize_soln_file); + Pass::call(design, "opt_clean"); } } } QbfSatPass; From 5527063f662cbb4b3be6af0f81b6877d58c5682e Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Thu, 26 Mar 2020 02:02:40 +0000 Subject: [PATCH 08/24] Add NDEBUG guards to `qbfsat` assertions. --- passes/sat/qbfsat.cc | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index c301e9e94..cbea94c9d 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -63,8 +63,10 @@ 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 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]+"); YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+"); +#endif YS_REGEX_MATCH_TYPE m; bool sat_regex_found = false; bool unsat_regex_found = false; @@ -73,8 +75,10 @@ void recover_solution(QbfSolutionType &sol) { if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { std::string loc = m[1].str(); std::string val = m[2].str(); +#ifndef NDEBUG log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex)); log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex)); +#endif sol.hole_to_value[loc] = val; } else if (YS_REGEX_NS::regex_search(x, sat_regex)) @@ -82,8 +86,10 @@ void recover_solution(QbfSolutionType &sol) { else if (YS_REGEX_NS::regex_search(x, unsat_regex)) unsat_regex_found = true; } +#ifndef NDEBUG log_assert(!sol.unknown && sol.sat? sat_regex_found : true); log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); +#endif } std::map get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { @@ -92,9 +98,11 @@ std::map get_hole_loc_name_map(RTLIL::Module *module, std::string cell_src = cell->get_src_attribute(); auto pos = sol.hole_to_value.find(cell_src); if (pos != sol.hole_to_value.end()) { +#ifndef NDEBUG log_assert(cell->type.in("$anyconst", "$anyseq")); log_assert(cell->hasPort(ID::Y)); log_assert(cell->getPort(ID::Y).is_wire()); +#endif hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); } } @@ -126,8 +134,10 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { std::string hole_value = m[2].str(); RTLIL::Wire *wire = module->wire(hole_name); +#ifndef NDEBUG log_assert(wire != nullptr); log_assert(wire->width > 0 && hole_value.size() == static_cast(wire->width)); +#endif log("Specializing %s from file with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); std::vector value_bv; @@ -145,13 +155,17 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { std::string hole_loc = it.first; std::string hole_value = it.second; +#ifndef NDEBUG auto pos = hole_loc_to_name.find(hole_loc); log_assert(pos != hole_loc_to_name.end()); +#endif std::string hole_name = hole_loc_to_name[hole_loc]; RTLIL::Wire *wire = module->wire(hole_name); +#ifndef NDEBUG log_assert(wire != nullptr); log_assert(wire->width > 0 && hole_value.size() == static_cast(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()); std::vector value_bv; @@ -166,7 +180,9 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { void allconstify_inputs(RTLIL::Module *module, const std::set &input_wires) { for(auto &n : input_wires) { RTLIL::Wire *input = module->wire(n); +#ifndef NDEBUG log_assert(input != nullptr); +#endif RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst"); allconst->setParam(ID(WIDTH), input->width); @@ -186,7 +202,9 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { std::string tempdir_name = "/tmp/yosys-z3-XXXXXX"; tempdir_name = make_temp_dir(tempdir_name); 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); //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 ]` From bb101e0b3a52a6040f41e53dbfb9067c67a1be23 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 27 Mar 2020 01:32:53 +0000 Subject: [PATCH 09/24] Implement the `-assume-outputs`, `-sat`, and -unsat` options for the `qbfsat` command. --- passes/sat/qbfsat.cc | 69 ++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 66 insertions(+), 3 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index cbea94c9d..11c91597e 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -49,14 +49,16 @@ struct QbfSolutionType { }; struct QbfSolveOptions { - bool timeout, specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2; + bool timeout, specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs; + bool sat, unsat; long timeout_sec; std::string specialize_soln_file; std::string write_soln_soln_file; std::string dump_final_smt2_file; size_t argidx; QbfSolveOptions() : timeout(false), specialize(false), specialize_from_file(false), write_solution(false), - nocleanup(false), dump_final_smt2(false), timeout_sec(-1), argidx(0) {}; + nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false), + timeout_sec(-1), argidx(0) {}; }; void recover_solution(QbfSolutionType &sol) { @@ -178,7 +180,7 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { } void allconstify_inputs(RTLIL::Module *module, const std::set &input_wires) { - for(auto &n : input_wires) { + for (auto &n : input_wires) { RTLIL::Wire *input = module->wire(n); #ifndef NDEBUG log_assert(input != nullptr); @@ -194,6 +196,40 @@ void allconstify_inputs(RTLIL::Module *module, const std::set &inpu module->fixup_ports(); } +void assume_miter_outputs(RTLIL::Module *module) { + std::vector wires_to_assume; + for (auto w : module->wires()) + if (w->port_output) { + if (w->width == 1) + wires_to_assume.push_back(w); + } + if (wires_to_assume.size() == 0) + return; + else { + log("Adding $assume cell for outputs: "); + for (auto w : wires_to_assume) + log("\"%s\" ", w->name.c_str()); + log("\n"); + } + + std::vector::size_type i; + while (wires_to_assume.size() > 1) { + std::vector buf; + for (i = 0; i + 1 < wires_to_assume.size(); i += 2) { + std::stringstream strstr; strstr << i; + RTLIL::Wire *and_wire = module->addWire("\\_qbfsat_and_" + strstr.str(), 1); + module->addLogicAnd("$_qbfsat_and_" + strstr.str(), wires_to_assume[i], wires_to_assume[i+1], and_wire, false, wires_to_assume[i]->get_src_attribute()); + buf.push_back(and_wire); + } + wires_to_assume.swap(buf); + } + +#ifndef NDEBUG + log_assert(wires_to_assume.size() == 1); +#endif + module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1); +} + QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; @@ -322,6 +358,18 @@ QbfSolveOptions parse_args(const std::vector &args) { opt.specialize = true; continue; } + else if (args[opt.argidx] == "-assume-outputs") { + opt.assume_outputs = true; + continue; + } + else if (args[opt.argidx] == "-sat") { + opt.sat = true; + continue; + } + else if (args[opt.argidx] == "-unsat") { + opt.unsat = true; + continue; + } else if (args[opt.argidx] == "-dump-final-smt2") { opt.dump_final_smt2 = true; if (args.size() <= opt.argidx + 1) @@ -403,6 +451,15 @@ struct QbfSatPass : public Pass { log(" -dump-final-smt2 \n"); log(" Pass the --dump-smt2 option to yosys-smtbmc.\n"); log("\n"); + log(" -assume-outputs\n"); + log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n"); + log("\n"); + log(" -sat\n"); + log(" Generate an error if the solver does not return \"sat\".\n"); + log("\n"); + log(" -unsat\n"); + log(" Generate an error if the solver does not return \"unsat\".\n"); + log("\n"); log(" -specialize\n"); log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n"); log("\n"); @@ -440,6 +497,8 @@ struct QbfSatPass : public Pass { //Replace input wires with wires assigned $allconst cells. std::set input_wires = validate_design_and_get_inputs(module); allconstify_inputs(module, input_wires); + if (opt.assume_outputs) + assume_miter_outputs(module); QbfSolutionType ret = qbf_solve(module, opt); Pass::call(design, "design -load _qbfsat_tmp"); @@ -460,7 +519,11 @@ struct QbfSatPass : public Pass { specialize(module, ret); Pass::call(design, "opt_clean"); } + 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 { specialize_from_file(module, opt.specialize_soln_file); Pass::call(design, "opt_clean"); From acf96b6b0bb7dc04686d89a6dc3aafd19adcdb85 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 27 Mar 2020 01:36:04 +0000 Subject: [PATCH 10/24] Remove unimplemented `-timeout` option. --- passes/sat/qbfsat.cc | 20 ++++---------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 11c91597e..d249c7dde 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -49,16 +49,15 @@ struct QbfSolutionType { }; struct QbfSolveOptions { - bool timeout, specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs; + bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs; bool sat, unsat; - long timeout_sec; std::string specialize_soln_file; std::string write_soln_soln_file; std::string dump_final_smt2_file; size_t argidx; - QbfSolveOptions() : timeout(false), 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), sat(false), unsat(false), - timeout_sec(-1), argidx(0) {}; + argidx(0) {}; }; void recover_solution(QbfSolutionType &sol) { @@ -342,15 +341,7 @@ std::set validate_design_and_get_inputs(RTLIL::Module *module) { QbfSolveOptions parse_args(const std::vector &args) { QbfSolveOptions opt; for (opt.argidx = 1; opt.argidx < args.size(); opt.argidx++) { - if (args[opt.argidx] == "-timeout") { - opt.timeout = true; - if (args.size() <= opt.argidx + 1) - log_cmd_error("timeout not specified.\n"); - else - opt.timeout_sec = atol(args[++opt.argidx].c_str()); - continue; - } - else if (args[opt.argidx] == "-nocleanup") { + if (args[opt.argidx] == "-nocleanup") { opt.nocleanup = true; continue; } @@ -441,9 +432,6 @@ struct QbfSatPass : public Pass { log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n"); log("by default.\n"); log("\n"); - log(" -timeout \n"); - log(" Set the solver timeout to the specified number of seconds.\n"); - log("\n"); log(" -nocleanup\n"); log(" Do not delete temporary files and directories. Useful for\n"); log(" debugging.\n"); From 09b2264837bf0a2d7d2c9b35f88c2d5924fa4364 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 27 Mar 2020 16:44:05 +0000 Subject: [PATCH 11/24] Clean up manual casting. Co-Authored-By: David Shah --- passes/sat/qbfsat.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index d249c7dde..4c3e24505 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -137,7 +137,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { RTLIL::Wire *wire = module->wire(hole_name); #ifndef NDEBUG log_assert(wire != nullptr); - log_assert(wire->width > 0 && hole_value.size() == static_cast(wire->width)); + log_assert(wire->width > 0 && GetSize(hole_value) == wire->width); #endif log("Specializing %s from file with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); @@ -165,7 +165,7 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { RTLIL::Wire *wire = module->wire(hole_name); #ifndef NDEBUG log_assert(wire != nullptr); - log_assert(wire->width > 0 && hole_value.size() == static_cast(wire->width)); + 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()); From 86fc49a9d60f9ad4cdeec93663e7245a9fdf60c6 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 27 Mar 2020 22:03:06 +0000 Subject: [PATCH 12/24] Use internal `run_command()` API instead of `popen()`. Co-Authored-By: Claire Wolf --- passes/sat/qbfsat.cc | 64 +++++++++++--------------------------------- 1 file changed, 15 insertions(+), 49 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 4c3e24505..bbe2f3354 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -231,12 +231,11 @@ void assume_miter_outputs(RTLIL::Module *module) { QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; - std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; - std::string smtbmc_warning = "z3: WARNING:"; + const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; + const std::string smtbmc_warning = "z3: WARNING:"; - std::string tempdir_name = "/tmp/yosys-z3-XXXXXX"; - tempdir_name = make_temp_dir(tempdir_name); - std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2"; + 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 @@ -244,51 +243,18 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 ]` { - fflush(stdout); - bool keep_reading = true; - int status = 0; - int retval = 0; - char buf[1024] = {0}; - std::string linebuf = ""; - 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"; + 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](const std::string &line) { + ret.stdout.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 + log("smtbmc output: %s", line.c_str()); + }; + log("Launching \"%s\".\n", cmd.c_str()); - -#ifndef EMSCRIPTEN - FILE *f = popen(cmd.c_str(), "r"); - if (f == nullptr) - log_cmd_error("errno %d after popen() returned NULL.\n", errno); - while (keep_reading) { - keep_reading = (fgets(buf, sizeof(buf), f) != nullptr); - linebuf += buf; - memset(buf, 0, sizeof(buf)); - - auto pos = linebuf.find('\n'); - while (pos != std::string::npos) { - std::string line = linebuf.substr(0, pos); - linebuf.erase(0, pos + 1); - ret.stdout.push_back(line); - auto warning_pos = line.find(smtbmc_warning); - if(warning_pos != std::string::npos) - log_warning("%s\n", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); - else - log("smtbmc output: %s\n", line.c_str()); - - pos = linebuf.find('\n'); - } - } - status = pclose(f); -#endif - - if(WIFEXITED(status)) { - retval = WEXITSTATUS(status); - } - else if(WIFSIGNALED(status)) { - retval = WTERMSIG(status); - } - else if(WIFSTOPPED(status)) { - retval = WSTOPSIG(status); - } - + int retval = run_command(cmd, process_line); if (retval == 0) { ret.sat = true; ret.unknown = false; From 125a583c575747e07530b214c922ff6a17c5bb34 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 3 Apr 2020 16:43:41 +0000 Subject: [PATCH 13/24] Use the `-duplicate` option rather than `-save` and `-load` with an explicit name. Co-Authored-By: Claire Wolf --- passes/sat/qbfsat.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index bbe2f3354..3db84a579 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -446,7 +446,7 @@ 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 -save _qbfsat_tmp"); + Pass::call(design, "design -duplicate"); //Replace input wires with wires assigned $allconst cells. std::set input_wires = validate_design_and_get_inputs(module); @@ -455,7 +455,7 @@ struct QbfSatPass : public Pass { assume_miter_outputs(module); QbfSolutionType ret = qbf_solve(module, opt); - Pass::call(design, "design -load _qbfsat_tmp"); + Pass::call(design, "design -pop"); module = design->module(module_name); if (ret.unknown) From d311a8022292a9934c11ff9124a53932469974e6 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Fri, 27 Mar 2020 23:25:24 +0000 Subject: [PATCH 14/24] Clean up `qbfsat` command and fix AND-reduction of miter outputs. --- passes/sat/qbfsat.cc | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 3db84a579..2861ae452 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -198,10 +198,9 @@ void allconstify_inputs(RTLIL::Module *module, const std::set &inpu void assume_miter_outputs(RTLIL::Module *module) { std::vector wires_to_assume; for (auto w : module->wires()) - if (w->port_output) { - if (w->width == 1) - wires_to_assume.push_back(w); - } + if (w->port_output && w->width == 1) + wires_to_assume.push_back(w); + if (wires_to_assume.size() == 0) return; else { @@ -211,16 +210,19 @@ void assume_miter_outputs(RTLIL::Module *module) { log("\n"); } - std::vector::size_type i; + unsigned long i = 0; while (wires_to_assume.size() > 1) { std::vector buf; - for (i = 0; i + 1 < wires_to_assume.size(); i += 2) { - std::stringstream strstr; strstr << i; + for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) { + std::stringstream strstr; strstr << i << "_" << j; RTLIL::Wire *and_wire = module->addWire("\\_qbfsat_and_" + strstr.str(), 1); - module->addLogicAnd("$_qbfsat_and_" + strstr.str(), wires_to_assume[i], wires_to_assume[i+1], and_wire, false, wires_to_assume[i]->get_src_attribute()); + module->addLogicAnd("$_qbfsat_and_" + strstr.str(), wires_to_assume[j], wires_to_assume[j+1], and_wire, false, wires_to_assume[j]->get_src_attribute()); buf.push_back(and_wire); } + if (wires_to_assume.size() % 2 == 1) + buf.push_back(wires_to_assume[wires_to_assume.size() - 1]); wires_to_assume.swap(buf); + ++i; } #ifndef NDEBUG From 6af8b767b436e504a7d0e271dca2ae0d355841dd Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 1 Apr 2020 19:28:07 +0000 Subject: [PATCH 15/24] Use `log_push()` and `log_pop()` and show the satisfiable model when `-specialize` is not specified. Co-Authored-By: N. Engelhardt --- passes/sat/qbfsat.cc | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 2861ae452..833cab167 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -178,6 +178,29 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { } } +void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { + log("Satisfiable model:\n"); + std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + for (auto &it : sol.hole_to_value) { + std::string hole_loc = it.first; + std::string hole_value = it.second; + +#ifndef NDEBUG + auto pos = hole_loc_to_name.find(hole_loc); + log_assert(pos != hole_loc_to_name.end()); +#endif + + std::string hole_name = hole_loc_to_name[hole_loc]; + log("\t%s = %lu'b%s\n", hole_name.c_str(), hole_value.size(), hole_value.c_str()); + std::vector value_bv; + value_bv.reserve(hole_value.size()); + for (char c : hole_value) + value_bv.push_back(c == '1'? RTLIL::S1 : RTLIL::S0); + std::reverse(value_bv.begin(), value_bv.end()); + } + +} + void allconstify_inputs(RTLIL::Module *module, const std::set &input_wires) { for (auto &n : input_wires) { RTLIL::Wire *input = module->wire(n); @@ -242,6 +265,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { 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 ]` { @@ -445,6 +469,7 @@ struct QbfSatPass : public Pass { if (module == NULL) log_cmd_error("Can't perform QBF-SAT on an empty selection!\n"); + log_push(); if (!opt.specialize_from_file) { //Save the design to restore after modiyfing the current module. std::string module_name = module->name.str(); @@ -474,6 +499,8 @@ struct QbfSatPass : public Pass { if (opt.specialize) { specialize(module, ret); Pass::call(design, "opt_clean"); + } else { + dump_model(module, ret); } if (opt.unsat) log_cmd_error("expected problem to be UNSAT\n"); @@ -484,6 +511,7 @@ struct QbfSatPass : public Pass { specialize_from_file(module, opt.specialize_soln_file); Pass::call(design, "opt_clean"); } + log_pop(); } } QbfSatPass; From ce033a8e3654ba1f9be06b9bab8202cc5a7d5b2b Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 1 Apr 2020 19:32:44 +0000 Subject: [PATCH 16/24] Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`. --- passes/sat/qbfsat.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 833cab167..a16ee546f 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -507,6 +507,8 @@ struct QbfSatPass : public Pass { } 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 { specialize_from_file(module, opt.specialize_soln_file); Pass::call(design, "opt_clean"); From 8f0f13cad2b1bbf0b7849c95bec82c33375402b7 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 1 Apr 2020 19:42:45 +0000 Subject: [PATCH 17/24] Suppress `yosys-smtbmc` output unless the new `-show-smtbmc` option is provided. --- passes/sat/qbfsat.cc | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index a16ee546f..c4d56928d 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -50,14 +50,14 @@ struct QbfSolutionType { struct QbfSolveOptions { bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs; - bool sat, unsat; + bool sat, unsat, show_smtbmc; std::string specialize_soln_file; std::string write_soln_soln_file; std::string dump_final_smt2_file; size_t argidx; QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false), - argidx(0) {}; + show_smtbmc(false), argidx(0) {}; }; void recover_solution(QbfSolutionType &sol) { @@ -258,6 +258,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; 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"; @@ -270,13 +271,14 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { //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](const std::string &line) { + auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](const std::string &line) { ret.stdout.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) + if (warning_pos != std::string::npos) log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); else - log("smtbmc output: %s", line.c_str()); + if (show_smtbmc) + log("smtbmc output: %s", line.c_str()); }; log("Launching \"%s\".\n", cmd.c_str()); @@ -353,6 +355,10 @@ QbfSolveOptions parse_args(const std::vector &args) { opt.unsat = true; continue; } + else if (args[opt.argidx] == "-show-smtbmc") { + opt.show_smtbmc = true; + continue; + } else if (args[opt.argidx] == "-dump-final-smt2") { opt.dump_final_smt2 = true; if (args.size() <= opt.argidx + 1) @@ -440,6 +446,9 @@ struct QbfSatPass : public Pass { log(" -unsat\n"); log(" Generate an error if the solver does not return \"unsat\".\n"); log("\n"); + log(" -show-smtbmc\n"); + log(" Print the output from yosys-smtbmc.\n"); + log("\n"); log(" -specialize\n"); log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n"); log("\n"); From 1db73e8dd24842b62c694db96035e9d7687d03ae Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 1 Apr 2020 21:33:54 +0000 Subject: [PATCH 18/24] Gracefully report error when module has nothing to prove. --- passes/sat/qbfsat.cc | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index c4d56928d..bfc1ae161 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -300,10 +300,11 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { return ret; } -std::set validate_design_and_get_inputs(RTLIL::Module *module) { +std::set 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; std::set input_wires; for (auto wire : module->wires()) { if (wire->port_input) { @@ -319,14 +320,16 @@ std::set validate_design_and_get_inputs(RTLIL::Module *module) { if (cell->type == "$anyconst") found_hole = true; if (cell->type.in("$assert", "$assume")) - found_1bit_output = true; + 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) - log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\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; } @@ -485,7 +488,7 @@ struct QbfSatPass : public Pass { Pass::call(design, "design -duplicate"); //Replace input wires with wires assigned $allconst cells. - std::set input_wires = validate_design_and_get_inputs(module); + std::set input_wires = validate_design_and_get_inputs(module, opt); allconstify_inputs(module, input_wires); if (opt.assume_outputs) assume_miter_outputs(module); From 0ca3a8e94f9bff1e262e6bea1796cc125fa24b92 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 1 Apr 2020 22:19:24 +0000 Subject: [PATCH 19/24] Improve style in `passes/sat/qbfsat.cc`. --- passes/sat/qbfsat.cc | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index bfc1ae161..8b7ccc685 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -227,14 +227,13 @@ void assume_miter_outputs(RTLIL::Module *module) { if (wires_to_assume.size() == 0) return; else { - log("Adding $assume cell for outputs: "); + log("Adding $assume cell for output(s): "); for (auto w : wires_to_assume) log("\"%s\" ", w->name.c_str()); log("\n"); } - unsigned long i = 0; - while (wires_to_assume.size() > 1) { + for(auto i = 0; wires_to_assume.size() > 1; ++i) { std::vector buf; for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) { std::stringstream strstr; strstr << i << "_" << j; @@ -245,7 +244,6 @@ void assume_miter_outputs(RTLIL::Module *module) { if (wires_to_assume.size() % 2 == 1) buf.push_back(wires_to_assume[wires_to_assume.size() - 1]); wires_to_assume.swap(buf); - ++i; } #ifndef NDEBUG From 5fedd0931c6e749483b8ddb3d7672ddca9ac5310 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Sat, 4 Apr 2020 22:22:54 +0000 Subject: [PATCH 20/24] Use newly-renamed `-push-copy` option. --- passes/sat/qbfsat.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 8b7ccc685..798a8edbb 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -483,7 +483,7 @@ 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 -duplicate"); + Pass::call(design, "design -push-copy"); //Replace input wires with wires assigned $allconst cells. std::set input_wires = validate_design_and_get_inputs(module, opt); From 194354e1280b082c2d4066839010b9d250386bb7 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Tue, 7 Apr 2020 03:29:54 +0000 Subject: [PATCH 21/24] Remove `$anyconst` cells before specialization to eliminate warnings and the need to run `opt_clean`. --- passes/sat/qbfsat.cc | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 798a8edbb..b9b9267eb 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -124,6 +124,8 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std void specialize_from_file(RTLIL::Module *module, const std::string &file) { YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$"); YS_REGEX_MATCH_TYPE m; + std::set anyconsts_to_remove; + std::map hole_name_to_value; std::ifstream fin(file.c_str()); if (!fin) log_cmd_error("could not read solution file.\n"); @@ -133,7 +135,23 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { log_assert(YS_REGEX_NS::regex_search(buf, m, hole_assn_regex)); std::string hole_name = m[1].str(); std::string hole_value = m[2].str(); + hole_name_to_value[hole_name] = hole_value; + } + for (auto cell : module->cells()) + if (cell->type == "$anyconst") { + auto anyconst_port_y = cell->getPort(ID::Y).as_wire(); + if (anyconst_port_y == nullptr) + continue; + if (hole_name_to_value.find(anyconst_port_y->name.str()) != hole_name_to_value.end()) + anyconsts_to_remove.insert(cell); + } + for (auto cell : anyconsts_to_remove) + module->remove(cell); + + for (auto &it : hole_name_to_value) { + std::string hole_name = it.first; + std::string hole_value = it.second; RTLIL::Wire *wire = module->wire(hole_name); #ifndef NDEBUG log_assert(wire != nullptr); @@ -152,6 +170,13 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + std::set anyconsts_to_remove; + for (auto cell : module->cells()) + if (cell->type == "$anyconst") + if (hole_loc_to_name.find(cell->get_src_attribute()) != hole_loc_to_name.end()) + anyconsts_to_remove.insert(cell); + for (auto cell : anyconsts_to_remove) + module->remove(cell); for (auto &it : sol.hole_to_value) { std::string hole_loc = it.first; std::string hole_value = it.second; @@ -508,7 +533,6 @@ struct QbfSatPass : public Pass { } if (opt.specialize) { specialize(module, ret); - Pass::call(design, "opt_clean"); } else { dump_model(module, ret); } @@ -521,7 +545,6 @@ struct QbfSatPass : public Pass { log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); } else { specialize_from_file(module, opt.specialize_soln_file); - Pass::call(design, "opt_clean"); } log_pop(); } From de5e6fa56ada699ae13585791593eabce089b718 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Thu, 9 Apr 2020 07:40:03 +0000 Subject: [PATCH 22/24] Clean up `passes/sat/qbfsat.cc`. Makes various cosmetic fixes, removes superfluous `hasPort()` check, and uses `emplace_back()` instead of `push_back()`. --- passes/sat/qbfsat.cc | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index b9b9267eb..77a34ec40 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -56,8 +56,8 @@ struct QbfSolveOptions { std::string dump_final_smt2_file; size_t argidx; QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), - nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false), - show_smtbmc(false), argidx(0) {}; + nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false), + show_smtbmc(false), argidx(0) {}; }; void recover_solution(QbfSolutionType &sol) { @@ -101,7 +101,6 @@ std::map get_hole_loc_name_map(RTLIL::Module *module, if (pos != sol.hole_to_value.end()) { #ifndef NDEBUG log_assert(cell->type.in("$anyconst", "$anyseq")); - log_assert(cell->hasPort(ID::Y)); log_assert(cell->getPort(ID::Y).is_wire()); #endif hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); @@ -162,7 +161,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { std::vector value_bv; value_bv.reserve(wire->width); for (char c : hole_value) - value_bv.push_back(c == '1'? RTLIL::S1 : RTLIL::S0); + value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); std::reverse(value_bv.begin(), value_bv.end()); module->connect(wire, value_bv); } @@ -197,7 +196,7 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { std::vector value_bv; value_bv.reserve(wire->width); for (char c : hole_value) - value_bv.push_back(c == '1'? RTLIL::S1 : RTLIL::S0); + value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); std::reverse(value_bv.begin(), value_bv.end()); module->connect(wire, value_bv); } @@ -220,7 +219,7 @@ void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { std::vector value_bv; value_bv.reserve(hole_value.size()); for (char c : hole_value) - value_bv.push_back(c == '1'? RTLIL::S1 : RTLIL::S0); + value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); std::reverse(value_bv.begin(), value_bv.end()); } @@ -357,7 +356,6 @@ std::set validate_design_and_get_inputs(RTLIL::Module *module, cons return input_wires; } - QbfSolveOptions parse_args(const std::vector &args) { QbfSolveOptions opt; for (opt.argidx = 1; opt.argidx < args.size(); opt.argidx++) { @@ -488,20 +486,20 @@ struct QbfSatPass : public Pass { log("\n"); log("\n"); } + void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE { - log_header(design, "Executing QBF-SAT pass (solving QBF-SAT problems in the circuit).\n"); + log_header(design, "Executing QBFSAT pass (solving QBF-SAT problems in the circuit).\n"); QbfSolveOptions opt = parse_args(args); extra_args(args, opt.argidx, design); - - RTLIL::Module *module = NULL; + RTLIL::Module *module = nullptr; for (auto mod : design->selected_modules()) { if (module) 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)); module = mod; } - if (module == NULL) + if (module == nullptr) log_cmd_error("Can't perform QBF-SAT on an empty selection!\n"); log_push(); @@ -543,9 +541,8 @@ struct QbfSatPass : public Pass { 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 { + } else specialize_from_file(module, opt.specialize_soln_file); - } log_pop(); } } QbfSatPass; From 73bd7fb01d83d276e47fb181fd53b1c97c2c0111 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Sat, 11 Apr 2020 06:53:59 +0000 Subject: [PATCH 23/24] Use `dict` instead of `std::map`. --- passes/sat/qbfsat.cc | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 77a34ec40..8c0d63601 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -40,7 +40,7 @@ PRIVATE_NAMESPACE_BEGIN struct QbfSolutionType { std::vector stdout; - std::map hole_to_value; + dict hole_to_value; bool sat; bool unknown; //true if neither 'sat' nor 'unsat' bool success; //true if exit code 0 @@ -71,7 +71,7 @@ void recover_solution(QbfSolutionType &sol) { YS_REGEX_MATCH_TYPE m; bool sat_regex_found = false; bool unsat_regex_found = false; - std::map hole_value_recovered; + dict hole_value_recovered; for (const std::string &x : sol.stdout) { if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { std::string loc = m[1].str(); @@ -93,8 +93,8 @@ void recover_solution(QbfSolutionType &sol) { #endif } -std::map get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { - std::map hole_loc_to_name; +dict get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { + dict hole_loc_to_name; for (auto cell : module->cells()) { std::string cell_src = cell->get_src_attribute(); auto pos = sol.hole_to_value.find(cell_src); @@ -115,7 +115,7 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std if (!fout) log_cmd_error("could not open solution file for writing.\n"); - std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + dict hole_loc_to_name = get_hole_loc_name_map(module, sol); for(auto &x : sol.hole_to_value) fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl; } @@ -124,7 +124,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$"); YS_REGEX_MATCH_TYPE m; std::set anyconsts_to_remove; - std::map hole_name_to_value; + dict hole_name_to_value; std::ifstream fin(file.c_str()); if (!fin) log_cmd_error("could not read solution file.\n"); @@ -168,7 +168,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { } void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { - std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + dict hole_loc_to_name = get_hole_loc_name_map(module, sol); std::set anyconsts_to_remove; for (auto cell : module->cells()) if (cell->type == "$anyconst") @@ -204,7 +204,7 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { log("Satisfiable model:\n"); - std::map hole_loc_to_name = get_hole_loc_name_map(module, sol); + dict hole_loc_to_name = get_hole_loc_name_map(module, sol); for (auto &it : sol.hole_to_value) { std::string hole_loc = it.first; std::string hole_value = it.second; From e300766fb3fbcb3b22558e638f7f43f81f545153 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Sat, 11 Apr 2020 09:41:09 +0000 Subject: [PATCH 24/24] Use `pool` instead of `std::set`. --- passes/sat/qbfsat.cc | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 8c0d63601..44691425f 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -123,7 +123,7 @@ void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std void specialize_from_file(RTLIL::Module *module, const std::string &file) { YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$"); YS_REGEX_MATCH_TYPE m; - std::set anyconsts_to_remove; + pool anyconsts_to_remove; dict hole_name_to_value; std::ifstream fin(file.c_str()); if (!fin) @@ -169,7 +169,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { dict hole_loc_to_name = get_hole_loc_name_map(module, sol); - std::set anyconsts_to_remove; + pool anyconsts_to_remove; for (auto cell : module->cells()) if (cell->type == "$anyconst") if (hole_loc_to_name.find(cell->get_src_attribute()) != hole_loc_to_name.end()) @@ -225,7 +225,7 @@ void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { } -void allconstify_inputs(RTLIL::Module *module, const std::set &input_wires) { +void allconstify_inputs(RTLIL::Module *module, const pool &input_wires) { for (auto &n : input_wires) { RTLIL::Wire *input = module->wire(n); #ifndef NDEBUG @@ -322,12 +322,12 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { return ret; } -std::set validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { +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; - std::set input_wires; + pool input_wires; for (auto wire : module->wires()) { if (wire->port_input) { found_input = true; @@ -509,7 +509,7 @@ struct QbfSatPass : public Pass { Pass::call(design, "design -push-copy"); //Replace input wires with wires assigned $allconst cells. - std::set input_wires = validate_design_and_get_inputs(module, opt); + pool input_wires = validate_design_and_get_inputs(module, opt); allconstify_inputs(module, input_wires); if (opt.assume_outputs) assume_miter_outputs(module);