diff options
| -rw-r--r-- | CODEOWNERS | 1 | ||||
| -rw-r--r-- | passes/sat/qbfsat.cc | 261 | ||||
| -rw-r--r-- | passes/sat/qbfsat.h | 252 |
3 files changed, 266 insertions, 248 deletions
diff --git a/CODEOWNERS b/CODEOWNERS index a73779920..350a62120 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -33,5 +33,6 @@ misc/*.py @btut backends/firrtl @ucbjrl @azidar passes/sat/qbfsat.cc @boqwxp +passes/sat/qbfsat.h @boqwxp passes/cmds/exec.cc @boqwxp passes/cmds/printattrs.cc @boqwxp diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 136259558..e4dfcaa0c 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -1,4 +1,4 @@ -/* +/* -*- c++ -*- * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc> @@ -18,13 +18,8 @@ */ #include "kernel/yosys.h" -#include "kernel/celltypes.h" #include "kernel/consteval.h" -#include "kernel/log.h" -#include "kernel/rtlil.h" -#include "kernel/register.h" -#include <algorithm> -#include <numeric> +#include "qbfsat.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -36,156 +31,7 @@ static inline unsigned int difference(unsigned int a, unsigned int b) { return a - b; } -struct QbfSolutionType { - std::vector<std::string> stdout_lines; - dict<pool<std::string>, std::string> hole_to_value; - double solver_time; - bool sat; - bool unknown; //true if neither 'sat' nor 'unsat' - - QbfSolutionType() : solver_time(0.0), sat(false), unknown(true) {} -}; - -struct QbfSolveOptions { - bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg; - bool nooptimize, nobisection; - bool sat, unsat, show_smtbmc; - enum Solver{Z3, Yices, CVC4} solver; - enum OptimizationLevel{O0, O1, O2} oflag; - int timeout; - 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), assume_neg(false), - nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false), - solver(Yices), oflag(O0), timeout(0), argidx(0) {}; -}; - -std::string get_solver_name(const QbfSolveOptions &opt) { - if (opt.solver == opt.Solver::Z3) - return "z3"; - else if (opt.solver == opt.Solver::Yices) - return "yices"; - else if (opt.solver == opt.Solver::CVC4) - return "cvc4"; - else - log_cmd_error("unknown solver specified.\n"); - return ""; -} - -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 unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED"); - YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)"); - YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)"); - YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)"); - YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver"); - YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\""); - YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); -#ifndef NDEBUG - YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); - 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; - dict<std::string, bool> hole_value_recovered; - for (const std::string &x : sol.stdout_lines) { - 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 - auto locs = split_tokens(loc, "|"); - pool<std::string> loc_pool(locs.begin(), locs.end()); - sol.hole_to_value[loc_pool] = val; - } - else if (YS_REGEX_NS::regex_search(x, sat_regex)) { - sat_regex_found = true; - sol.sat = true; - sol.unknown = false; - } - else if (YS_REGEX_NS::regex_search(x, unsat_regex)) { - unsat_regex_found = true; - sol.sat = false; - sol.unknown = false; - } - else if (YS_REGEX_NS::regex_search(x, memout_regex)) { - sol.unknown = true; - log_warning("solver ran out of memory\n"); - } - else if (YS_REGEX_NS::regex_search(x, timeout_regex)) { - sol.unknown = true; - log_warning("solver timed out\n"); - } - else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) { - sol.unknown = true; - log_warning("solver timed out\n"); - } - else if (YS_REGEX_NS::regex_search(x, unknown_regex)) { - sol.unknown = true; - log_warning("solver returned \"unknown\"\n"); - } - else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) { - unsat_regex_found = true; - sol.sat = false; - sol.unknown = false; - } - else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) { - sol.unknown = true; - } - } -#ifndef NDEBUG - log_assert(!sol.unknown && sol.sat? sat_regex_found : true); - log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); -#endif -} - -dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module, const QbfSolutionType &sol) { - dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit; - pool<RTLIL::SigBit> anyconst_sigbits; - dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit; - - for (auto cell : module->cells()) { - pool<std::string> cell_src = cell->get_strpool_attribute(ID::src); - auto pos = sol.hole_to_value.find(cell_src); - if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) { - RTLIL::SigSpec port_y = cell->getPort(ID::Y); - for (int i = GetSize(port_y) - 1; i >= 0; --i) { - hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i]; - anyconst_sigbits.insert(port_y[i]); - } - } - } - - for (auto &conn : module->connections()) { - auto lhs = conn.first; - auto rhs = conn.second; - for (auto i = 0; i < GetSize(rhs); ++i) { - if (anyconst_sigbits[rhs[i]]) { - auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]); - if (pos != anyconst_sigbit_to_wire_sigbit.end()) - log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i])); - anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i]; - } - } - } - - for (auto &it : hole_loc_idx_to_sigbit) { - auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second); - if (pos != anyconst_sigbit_to_wire_sigbit.end()) - it.second = pos->second; - } - - return hole_loc_idx_to_sigbit; -} - -pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { +pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, bool assume_outputs) { bool found_input = false; bool found_hole = false; bool found_1bit_output = false; @@ -213,48 +59,12 @@ pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const Qb log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); if (!found_1bit_output && !found_assert_assume) log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); - if (!found_assert_assume && !opt.assume_outputs) + if (!found_assert_assume && !assume_outputs) log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n"); return input_wires; } -void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) { - std::ofstream fout(file.c_str()); - if (!fout) - log_cmd_error("could not open solution file for writing.\n"); - - //There is a question here: How exactly shall we identify holes? - //There are at least two reasonable options: - //1. By the source location of the $anyconst cells - //2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec. - // - //Option 1 has the benefit of being very precise. There is very limited potential for confusion, as long - //as the source attribute has been set. However, if the source attribute is not set, this won't work. - //More importantly, we want to have the ability to port hole assignments to other modules with compatible - //hole names and widths. Obviously in those cases source locations of the $anyconst cells will not match. - // - //Option 2 has the benefits previously described, but wire names can be changed automatically by - //optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC. - // - //The approach taken here is to allow both options. We write the assignment information for each bit of - //the solution on a separate line. Each line is of one of two forms: - // - //location bit name = value - //location bit name [offset] = value - // - //where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute, - //"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding - //to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same - //SigBit, and "value", which is either '0' or '1', represents the assignment for that bit. - dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol); - for (auto &x : sol.hole_to_value) { - std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;}); - for (auto i = 0; i < GetSize(x.second); ++i) - fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl; - } -} - void specialize_from_file(RTLIL::Module *module, const std::string &file) { YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$"); YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified @@ -318,7 +128,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { } void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) { - dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol); + auto hole_loc_idx_to_sigbit = sol.get_hole_loc_idx_sigbit_map(module); pool<RTLIL::Cell *> anyconsts_to_remove; for (auto cell : module->cells()) if (cell->type == "$anyconst") @@ -348,24 +158,6 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = } } -void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { - log("Satisfiable model:\n"); - dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module, sol); - for (auto &it : sol.hole_to_value) { - pool<std::string> hole_loc = it.first; - std::string hole_value = it.second; - - for (unsigned int i = 0; i < hole_value.size(); ++i) { - int bit_idx = GetSize(hole_value) - 1 - i; - auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i)); - log_assert(it != hole_loc_idx_to_sigbit.end()); - - RTLIL::SigBit hole_sigbit = it->second; - log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]); - } - } -} - void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) { for (auto &n : input_wires) { RTLIL::Wire *input = module->wire(n); @@ -383,7 +175,7 @@ void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wi module->fixup_ports(); } -void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { +void assume_miter_outputs(RTLIL::Module *module, bool assume_neg) { std::vector<RTLIL::Wire *> wires_to_assume; for (auto w : module->wires()) if (w->port_output && w->width == 1) @@ -398,7 +190,7 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { log("\n"); } - if (opt.assume_neg) { + if (assume_neg) { for (unsigned int i = 0; i < wires_to_assume.size(); ++i) { RTLIL::SigSpec n_wire = module->LogicNot(wires_to_assume[i]->name.str() + "__n__qbfsat", wires_to_assume[i], false, wires_to_assume[i]->get_src_attribute()); wires_to_assume[i] = n_wire.as_wire(); @@ -430,7 +222,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2"; const std::string smtbmc_warning = "z3: WARNING:"; - const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1"; + const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (opt.get_solver_name()) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1"; Pass::call(mod->design, smt2_command); @@ -451,7 +243,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, ret.solver_time = (end - begin) / 1e9f; if (!quiet) log("Solver finished in %.3f seconds.\n", ret.solver_time); - recover_solution(ret); + ret.recover_solution(); return ret; } @@ -468,10 +260,10 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { Pass::call(design, "design -push-copy"); //Replace input wires with wires assigned $allconst cells: - pool<std::string> input_wires = validate_design_and_get_inputs(module, opt); + pool<std::string> input_wires = validate_design_and_get_inputs(module, opt.assume_outputs); allconstify_inputs(module, input_wires); if (opt.assume_outputs) - assume_miter_outputs(module, opt); + assume_miter_outputs(module, opt.assume_neg); //Find the wire to be optimized, if any: for (auto wire : module->wires()) { @@ -699,33 +491,6 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { return opt; } -void print_proof_failed() -{ - log("\n"); - 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() override @@ -827,12 +592,12 @@ struct QbfSatPass : public Pass { else if (ret.sat) { print_qed(); if (opt.write_solution) { - write_solution(module, ret, opt.write_soln_soln_file); + ret.write_solution(module, opt.write_soln_soln_file); } if (opt.specialize) { specialize(module, ret); } else { - dump_model(module, ret); + ret.dump_model(module); } if (opt.unsat) log_cmd_error("expected problem to be UNSAT\n"); diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h new file mode 100644 index 000000000..401f9c7a6 --- /dev/null +++ b/passes/sat/qbfsat.h @@ -0,0 +1,252 @@ +/* -*- c++ -*- + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc> + * + * 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. + * + */ + +#ifndef QBFSAT_H +#define QBFSAT_H + +#include "kernel/yosys.h" +#include <numeric> + +YOSYS_NAMESPACE_BEGIN + +struct QbfSolveOptions { + bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false; + bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false; + bool nobisection = false, sat = false, unsat = false, show_smtbmc = false; + enum Solver{Z3, Yices, CVC4} solver = Yices; + enum OptimizationLevel{O0, O1, O2} oflag = O0; + int timeout = 0; + std::string specialize_soln_file = ""; + std::string write_soln_soln_file = ""; + std::string dump_final_smt2_file = ""; + size_t argidx = 0; + + std::string get_solver_name() const { + if (solver == Solver::Z3) + return "z3"; + else if (solver == Solver::Yices) + return "yices"; + else if (solver == Solver::CVC4) + return "cvc4"; + + log_cmd_error("unknown solver specified.\n"); + return ""; + } +}; + +struct QbfSolutionType { + std::vector<std::string> stdout_lines = {}; + dict<pool<std::string>, std::string> hole_to_value = {}; + double solver_time = 0; + bool sat = false; + bool unknown = true; //true if neither 'sat' nor 'unsat' + + dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module) const { + dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit; + pool<RTLIL::SigBit> anyconst_sigbits; + dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit; + + for (auto cell : module->cells()) { + pool<std::string> cell_src = cell->get_strpool_attribute(ID::src); + auto pos = hole_to_value.find(cell_src); + if (pos != hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) { + RTLIL::SigSpec port_y = cell->getPort(ID::Y); + for (int i = GetSize(port_y) - 1; i >= 0; --i) { + hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i]; + anyconst_sigbits.insert(port_y[i]); + } + } + } + + for (auto &conn : module->connections()) { + auto lhs = conn.first; + auto rhs = conn.second; + for (auto i = 0; i < GetSize(rhs); ++i) { + if (anyconst_sigbits[rhs[i]]) { + auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]); + if (pos != anyconst_sigbit_to_wire_sigbit.end()) + log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i])); + anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i]; + } + } + } + + for (auto &it : hole_loc_idx_to_sigbit) { + auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second); + if (pos != anyconst_sigbit_to_wire_sigbit.end()) + it.second = pos->second; + } + + return hole_loc_idx_to_sigbit; + } + + void dump_model(RTLIL::Module *module) const { + log("Satisfiable model:\n"); + auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module); + for (auto &it : hole_to_value) { + pool<std::string> hole_loc = it.first; + std::string hole_value = it.second; + + for (unsigned int i = 0; i < hole_value.size(); ++i) { + int bit_idx = GetSize(hole_value) - 1 - i; + auto it = hole_loc_idx_to_sigbit.find(std::make_pair(hole_loc, i)); + log_assert(it != hole_loc_idx_to_sigbit.end()); + + RTLIL::SigBit hole_sigbit = it->second; + log("\t%s = 1'b%c\n", log_signal(hole_sigbit), hole_value[bit_idx]); + } + } + } + + void write_solution(RTLIL::Module *module, const std::string &file) const { + std::ofstream fout(file.c_str()); + if (!fout) + log_cmd_error("could not open solution file for writing.\n"); + + //There is a question here: How exactly shall we identify holes? + //There are at least two reasonable options: + //1. By the source location of the $anyconst cells + //2. By the name(s) of the wire(s) connected to each SigBit of the $anyconst cell->getPort(ID::Y) SigSpec. + // + //Option 1 has the benefit of being very precise. There is very limited potential for confusion, as long + //as the source attribute has been set. However, if the source attribute is not set, this won't work. + //More importantly, we want to have the ability to port hole assignments to other modules with compatible + //hole names and widths. Obviously in those cases source locations of the $anyconst cells will not match. + // + //Option 2 has the benefits previously described, but wire names can be changed automatically by + //optimization or techmapping passes, especially when (ex/im)porting from BLIF for optimization with ABC. + // + //The approach taken here is to allow both options. We write the assignment information for each bit of + //the solution on a separate line. Each line is of one of two forms: + // + //location bit name = value + //location bit name [offset] = value + // + //where '[', ']', and '=' are literal symbols, "location" is the $anyconst cell source location attribute, + //"bit" is the index of the $anyconst cell, "name" is the `wire->name` field of the SigBit corresponding + //to the current bit of the $anyconst cell->getPort(ID::Y), "offset" is the `offset` field of that same + //SigBit, and "value", which is either '0' or '1', represents the assignment for that bit. + auto hole_loc_idx_to_sigbit = get_hole_loc_idx_sigbit_map(module); + for (auto &x : hole_to_value) { + std::string src_as_str = std::accumulate(x.first.begin(), x.first.end(), std::string(), [](const std::string &a, const std::string &b){return a + "|" + b;}); + for (auto i = 0; i < GetSize(x.second); ++i) + fout << src_as_str.c_str() << " " << i << " " << log_signal(hole_loc_idx_to_sigbit[std::make_pair(x.first, i)]) << " = " << x.second[GetSize(x.second) - 1 - i] << std::endl; + } + } + + void recover_solution() { + 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 unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED"); + YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)"); + YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)"); + YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)"); + YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver"); + YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\""); + YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); +#ifndef NDEBUG + YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); + 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; + dict<std::string, bool> hole_value_recovered; + for (const std::string &x : stdout_lines) { + 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 + auto locs = split_tokens(loc, "|"); + pool<std::string> loc_pool(locs.begin(), locs.end()); + hole_to_value[loc_pool] = val; + } + else if (YS_REGEX_NS::regex_search(x, sat_regex)) { + sat_regex_found = true; + sat = true; + unknown = false; + } + else if (YS_REGEX_NS::regex_search(x, unsat_regex)) { + unsat_regex_found = true; + sat = false; + unknown = false; + } + else if (YS_REGEX_NS::regex_search(x, memout_regex)) { + unknown = true; + log_warning("solver ran out of memory\n"); + } + else if (YS_REGEX_NS::regex_search(x, timeout_regex)) { + unknown = true; + log_warning("solver timed out\n"); + } + else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) { + unknown = true; + log_warning("solver timed out\n"); + } + else if (YS_REGEX_NS::regex_search(x, unknown_regex)) { + unknown = true; + log_warning("solver returned \"unknown\"\n"); + } + else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) { + unsat_regex_found = true; + sat = false; + unknown = false; + } + else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) { + unknown = true; + } + } + log_assert(!unknown && sat? sat_regex_found : true); + log_assert(!unknown && !sat? unsat_regex_found : true); + } +}; + +void print_proof_failed() +{ + log("\n"); + 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"); +} + +YOSYS_NAMESPACE_END + +#endif |