diff options
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/assertpmux.cc | 4 | ||||
| -rw-r--r-- | passes/sat/async2sync.cc | 4 | ||||
| -rw-r--r-- | passes/sat/clk2fflogic.cc | 4 | ||||
| -rw-r--r-- | passes/sat/cutpoint.cc | 23 | ||||
| -rw-r--r-- | passes/sat/eval.cc | 4 | ||||
| -rw-r--r-- | passes/sat/expose.cc | 34 | ||||
| -rw-r--r-- | passes/sat/fmcombine.cc | 7 | ||||
| -rw-r--r-- | passes/sat/fminit.cc | 4 | ||||
| -rw-r--r-- | passes/sat/freduce.cc | 4 | ||||
| -rw-r--r-- | passes/sat/miter.cc | 4 | ||||
| -rw-r--r-- | passes/sat/mutate.cc | 4 | ||||
| -rw-r--r-- | passes/sat/qbfsat.cc | 654 | ||||
| -rw-r--r-- | passes/sat/qbfsat.h | 252 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 12 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 9 | ||||
| -rw-r--r-- | passes/sat/supercover.cc | 4 |
16 files changed, 676 insertions, 351 deletions
diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc index 5bf2296ab..e9a10465e 100644 --- a/passes/sat/assertpmux.cc +++ b/passes/sat/assertpmux.cc @@ -181,7 +181,7 @@ struct AssertpmuxWorker struct AssertpmuxPass : public Pass { AssertpmuxPass() : Pass("assertpmux", "adds asserts for parallel muxes") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -199,7 +199,7 @@ struct AssertpmuxPass : public Pass { log(" additional constraint and check the $pmux condition always.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { bool flag_noinit = false; bool flag_always = false; diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index e344e2b5b..6fc480925 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct Async2syncPass : public Pass { Async2syncPass() : Pass("async2sync", "convert async FF inputs to sync circuits") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -42,7 +42,7 @@ struct Async2syncPass : public Pass { log("Currently only $adff, $dffsr, and $dlatch cells are supported by this pass.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { // bool flag_noinit = false; diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index 1e155e52c..e5c5d0486 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct Clk2fflogicPass : public Pass { Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -36,7 +36,7 @@ struct Clk2fflogicPass : public Pass { log("multiple clocks.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { // bool flag_noinit = false; diff --git a/passes/sat/cutpoint.cc b/passes/sat/cutpoint.cc index 26cc69211..6fc267d51 100644 --- a/passes/sat/cutpoint.cc +++ b/passes/sat/cutpoint.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct CutpointPass : public Pass { CutpointPass() : Pass("cutpoint", "adds formal cut points to the design") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -38,7 +38,7 @@ struct CutpointPass : public Pass { log(" $anyseq cell and drive the cutpoint net from that\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { bool flag_undef = false; @@ -126,15 +126,16 @@ struct CutpointPass : public Pass { } vector<Wire*> rewrite_wires; - for (auto wire : module->wires()) { - if (!wire->port_input) - continue; - int bit_count = 0; - for (auto &bit : sigmap(wire)) - if (cutpoint_bits.count(bit)) - bit_count++; - if (bit_count) - rewrite_wires.push_back(wire); + for (auto id : module->ports) { + RTLIL::Wire *wire = module->wire(id); + if (wire->port_input) { + int bit_count = 0; + for (auto &bit : sigmap(wire)) + if (cutpoint_bits.count(bit)) + bit_count++; + if (bit_count) + rewrite_wires.push_back(wire); + } } for (auto wire : rewrite_wires) { diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index f910ea80d..085e7c5b8 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -359,7 +359,7 @@ struct VlogHammerReporter struct EvalPass : public Pass { EvalPass() : Pass("eval", "evaluate the circuit given an input") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -382,7 +382,7 @@ struct EvalPass : public Pass { log(" then all output ports of the current module are used.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { std::vector<std::pair<std::string, std::string>> sets; std::vector<std::string> shows, tables; diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc index 80ab82cd5..2c65821cf 100644 --- a/passes/sat/expose.cc +++ b/passes/sat/expose.cc @@ -217,7 +217,7 @@ RTLIL::Wire *add_new_wire(RTLIL::Module *module, RTLIL::IdString name, int width struct ExposePass : public Pass { ExposePass() : Pass("expose", "convert internal signals to module ports") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -254,7 +254,7 @@ struct ExposePass : public Pass { log(" designator for the exposed signal.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { bool flag_shared = false; bool flag_evert = false; @@ -281,11 +281,15 @@ struct ExposePass : public Pass { flag_dff = true; continue; } - if (args[argidx] == "-cut" && !flag_input) { + if (args[argidx] == "-cut") { + if (flag_input) + log_cmd_error("Options -cut and -input are mutually exclusive.\n"); flag_cut = true; continue; } - if (args[argidx] == "-input" && !flag_cut) { + if (args[argidx] == "-input") { + if (flag_cut) + log_cmd_error("Options -cut and -input are mutually exclusive.\n"); flag_input = true; continue; } @@ -445,6 +449,8 @@ struct ExposePass : public Pass { SigMap out_to_in_map; + std::map<RTLIL::Wire*, RTLIL::IdString> wire_map; + for (auto w : module->wires()) { if (flag_shared) { @@ -462,8 +468,7 @@ struct ExposePass : public Pass { if (!w->port_input) { w->port_input = true; log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name)); - RTLIL::Wire *in_wire = module->addWire(NEW_ID, GetSize(w)); - out_to_in_map.add(w, in_wire); + wire_map[w] = NEW_ID; } } else @@ -474,15 +479,19 @@ struct ExposePass : public Pass { } if (flag_cut) { - RTLIL::Wire *in_wire = add_new_wire(module, w->name.str() + sep + "i", w->width); - in_wire->port_input = true; - out_to_in_map.add(sigmap(w), in_wire); + wire_map[w] = w->name.str() + sep + "i"; } } } if (flag_input) { + for (auto &wm : wire_map) + { + RTLIL::Wire *in_wire = module->addWire(wm.second, GetSize(wm.first)); + out_to_in_map.add(wm.first, in_wire); + } + for (auto cell : module->cells()) { if (!ct.cell_known(cell->type)) continue; @@ -497,6 +506,13 @@ struct ExposePass : public Pass { if (flag_cut) { + for (auto &wm : wire_map) + { + RTLIL::Wire *in_wire = add_new_wire(module, wm.second, wm.first->width); + in_wire->port_input = true; + out_to_in_map.add(sigmap(wm.first), in_wire); + } + for (auto cell : module->cells()) { if (!ct.cell_known(cell->type)) continue; diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc index 5066485aa..cb49edac3 100644 --- a/passes/sat/fmcombine.cc +++ b/passes/sat/fmcombine.cc @@ -114,8 +114,7 @@ struct FmcombineWorker Cell *gold = import_prim_cell(cell, "_gold"); Cell *gate = import_prim_cell(cell, "_gate"); if (opts.initeq) { - if (cell->type.in(ID($ff), ID($dff), ID($dffe), - ID($dffsr), ID($adff), ID($dlatch), ID($dlatchsr))) { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) { SigSpec gold_q = gold->getPort(ID::Q); SigSpec gate_q = gate->getPort(ID::Q); SigSpec en = module->Initstate(NEW_ID); @@ -235,7 +234,7 @@ struct FmcombineWorker struct FmcombinePass : public Pass { FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -272,7 +271,7 @@ struct FmcombinePass : public Pass { log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { opts_t opts; Module *module = nullptr; diff --git a/passes/sat/fminit.cc b/passes/sat/fminit.cc index 555a28dc6..c72e62548 100644 --- a/passes/sat/fminit.cc +++ b/passes/sat/fminit.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct FminitPass : public Pass { FminitPass() : Pass("fminit", "set init values/sequences for formal") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -47,7 +47,7 @@ struct FminitPass : public Pass { log(" Set clock for init sequences\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { vector<pair<string, vector<string>>> initdata; vector<pair<string, string>> setdata; diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index 5dfd7bd3f..762edfdfb 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -760,7 +760,7 @@ struct FreduceWorker struct FreducePass : public Pass { FreducePass() : Pass("freduce", "perform functional reduction") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -791,7 +791,7 @@ struct FreducePass : public Pass { log("circuit that is analyzed.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { reduce_counter = 0; reduce_stop_at = 0; diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index aeece9b94..fe4a819f3 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -354,7 +354,7 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL struct MiterPass : public Pass { MiterPass() : Pass("miter", "automatically create a miter circuit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -398,7 +398,7 @@ struct MiterPass : public Pass { log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { if (args.size() > 1 && args[1] == "-equiv") { create_miter_equiv(this, args, design); diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index af8ffca9e..15abee73e 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -726,7 +726,7 @@ void mutate_cnot(Design *design, const mutate_opts_t &opts, bool one) struct MutatePass : public Pass { MutatePass() : Pass("mutate", "generate or apply design mutations") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -790,7 +790,7 @@ struct MutatePass : public Pass { log(" Ignored. (They are generated by -list for documentation purposes.)\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { mutate_opts_t opts; string filename; diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index d99ca1b53..46f7f5070 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,216 +18,149 @@ */ #include "kernel/yosys.h" -#include "kernel/celltypes.h" -#include "kernel/log.h" -#include "kernel/rtlil.h" -#include "kernel/register.h" -#include <cstdio> -#include <algorithm> - -#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 <sys/wait.h> -#endif +#include "kernel/consteval.h" +#include "qbfsat.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct QbfSolutionType { - std::vector<std::string> stdout_lines; - dict<std::string, std::string> hole_to_value; - bool sat; - bool unknown; //true if neither 'sat' nor 'unsat' - bool success; //true if exit code 0 - - QbfSolutionType() : sat(false), unknown(true), success(false) {} -}; - -struct QbfSolveOptions { - bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg; - 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), assume_neg(false), - sat(false), unsat(false), show_smtbmc(false), argidx(0) {}; -}; - -void recover_solution(QbfSolutionType &sol) { - YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); - YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); - YS_REGEX_TYPE 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 - 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; - } -#ifndef NDEBUG - log_assert(!sol.unknown && sol.sat? sat_regex_found : true); - log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true); -#endif +static inline unsigned int difference(unsigned int a, unsigned int b) { + if (a < b) + return b - a; + else + return a - b; } -dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) { - dict<std::string, std::string> 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); - if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) { - log_assert(hole_loc_to_name.find(pos->first) == hole_loc_to_name.end()); - hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str(); +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; + bool found_assert_assume = false; + pool<std::string> input_wires; + for (auto wire : module->wires()) { + if (wire->port_input) { + found_input = true; + input_wires.insert(wire->name.str()); } + if (wire->port_output && wire->width == 1) + found_1bit_output = true; } + for (auto cell : module->cells()) { + if (cell->type == "$allconst") + found_input = true; + if (cell->type == "$anyconst") + found_hole = true; + if (cell->type.in("$assert", "$assume")) + found_assert_assume = true; + } + if (!found_input) + log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n"); + if (!found_hole) + log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); + if (!found_1bit_output && !found_assert_assume) + log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); + if (!found_assert_assume && !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 hole_loc_to_name; + 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"); +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 + YS_REGEX_MATCH_TYPE bit_m, m; + dict<pool<std::string>, RTLIL::Cell*> anyconst_loc_to_cell; + dict<RTLIL::SigBit, RTLIL::State> hole_assignments; - dict<std::string, std::string> 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; -} + for (auto cell : module->cells()) + if (cell->type == "$anyconst") + anyconst_loc_to_cell[cell->get_strpool_attribute(ID::src)] = cell; -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; - pool<RTLIL::Cell *> anyconsts_to_remove; - dict<std::string, std::string> hole_name_to_value; 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(); - hole_name_to_value[hole_name] = hole_value; - } + bool bit_assn = true; + if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) { + bit_assn = false; + if (!YS_REGEX_NS::regex_search(buf, m, hole_assn_regex)) + log_cmd_error("solution file is not formatted correctly: \"%s\"\n", buf.c_str()); + } - 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); + std::string hole_loc = bit_assn? bit_m[1].str() : m[1].str(); + unsigned int hole_bit = bit_assn? atoi(bit_m[2].str().c_str()) : atoi(m[2].str().c_str()); + std::string hole_name = bit_assn? bit_m[3].str() : m[3].str(); + unsigned int hole_offset = bit_assn? atoi(bit_m[4].str().c_str()) : 0; + RTLIL::State hole_value = bit_assn? (atoi(bit_m[5].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0) + : (atoi(m[4].str().c_str()) == 1? RTLIL::State::S1 : RTLIL::State::S0); + + //We have two options to identify holes. First, try to match wire names. If we can't find a matching wire, + //then try to find a cell with a matching location. + RTLIL::SigBit hole_sigbit; + if (module->wire(hole_name) != nullptr) { + RTLIL::Wire *hole_wire = module->wire(hole_name); + hole_sigbit = RTLIL::SigSpec(hole_wire)[hole_offset]; + } else { + auto locs = split_tokens(hole_loc, "|"); + pool<std::string> hole_loc_pool(locs.begin(), locs.end()); + auto hole_cell_it = anyconst_loc_to_cell.find(hole_loc_pool); + if (hole_cell_it == anyconst_loc_to_cell.end()) + log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str()); + + RTLIL::Cell *hole_cell = hole_cell_it->second; + hole_sigbit = hole_cell->getPort(ID::Y)[hole_bit]; } - for (auto cell : anyconsts_to_remove) - module->remove(cell); + hole_assignments[hole_sigbit] = hole_value; + } - 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); - 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()); - std::vector<RTLIL::SigBit> value_bv; - value_bv.reserve(wire->width); - for (char c : hole_value) - value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); - std::reverse(value_bv.begin(), value_bv.end()); - module->connect(wire, value_bv); + for (auto &it : anyconst_loc_to_cell) + module->remove(it.second); + + for (auto &it : hole_assignments) { + RTLIL::SigSpec lhs(it.first); + RTLIL::SigSpec rhs(it.second); + log("Specializing %s from file with %s = %d.\n", module->name.c_str(), log_signal(it.first), it.second == RTLIL::State::S1? 1 : 0); + module->connect(lhs, rhs); } } -void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { - dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol); +void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) { + 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") - if (hole_loc_to_name.find(cell->get_src_attribute()) != hole_loc_to_name.end()) + if (hole_loc_idx_to_sigbit.find(std::make_pair(cell->get_strpool_attribute(ID::src), 0)) != hole_loc_idx_to_sigbit.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; - -#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 && 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()); - std::vector<RTLIL::SigBit> value_bv; - value_bv.reserve(wire->width); - for (char c : hole_value) - value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); - std::reverse(value_bv.begin(), value_bv.end()); - module->connect(wire, value_bv); - } -} - -void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { - log("Satisfiable model:\n"); - dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol); - for (auto &it : sol.hole_to_value) { - std::string hole_loc = it.first; + pool<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<RTLIL::SigBit> value_bv; - value_bv.reserve(hole_value.size()); - for (char c : hole_value) - value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); - std::reverse(value_bv.begin(), value_bv.end()); + 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_assert(hole_sigbit.wire != nullptr); + log_assert(hole_value[bit_idx] == '0' || hole_value[bit_idx] == '1'); + RTLIL::SigSpec lhs(hole_sigbit.wire, hole_sigbit.offset, 1); + RTLIL::State hole_bit_val = hole_value[bit_idx] == '1'? RTLIL::State::S1 : RTLIL::State::S0; + if (!quiet) + log("Specializing %s with %s = %d.\n", module->name.c_str(), log_signal(hole_sigbit), hole_bit_val == RTLIL::State::S0? 0 : 1) +; + module->connect(lhs, hole_bit_val); + } } - } void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &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); @@ -239,7 +172,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) @@ -254,7 +187,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(); @@ -274,90 +207,173 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { 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 call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, const std::string &tempdir_name, const bool quiet = false, const int iter_num = 0) { + //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]` QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; + const std::string smt2_command = stringf("write_smt2 -stbv -wires %s/problem%d.smt2", tempdir_name.c_str(), iter_num); const std::string smtbmc_warning = "z3: WARNING:"; - const bool show_smtbmc = opt.show_smtbmc; + const std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1", + yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(), + (opt.timeout != 0? stringf("--timeout %d", opt.timeout) : "").c_str(), + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(), + tempdir_name.c_str(), iter_num); - const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX"); - const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2"; -#ifndef NDEBUG - log_assert(mod->design != nullptr); -#endif Pass::call(mod->design, smt2_command); + + auto process_line = [&ret, &smtbmc_warning, &opt, &quiet](const std::string &line) { + ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline + auto warning_pos = line.find(smtbmc_warning); + if (warning_pos != std::string::npos) + log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); + else + if (opt.show_smtbmc && !quiet) + log("smtbmc output: %s", line.c_str()); + }; log_header(mod->design, "Solving QBF-SAT problem.\n"); + if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str()); + int64_t begin = PerformanceTimer::query(); + run_command(smtbmc_cmd, process_line); + int64_t end = PerformanceTimer::query(); + ret.solver_time = (end - begin) / 1e9f; + if (!quiet) log("Solver finished in %.3f seconds.\n", ret.solver_time); + + ret.recover_solution(); + return ret; +} - //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]` - { - const std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1"; - auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](const std::string &line) { - ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline - auto warning_pos = line.find(smtbmc_warning); - if (warning_pos != std::string::npos) - log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); - else - if (show_smtbmc) - log("smtbmc output: %s", line.c_str()); - }; - - log("Launching \"%s\".\n", cmd.c_str()); - int retval = run_command(cmd, process_line); - if (retval == 0) { - ret.sat = true; - ret.unknown = false; - } else if (retval == 1) { - ret.sat = false; - ret.unknown = false; +QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { + QbfSolutionType ret, best_soln; + const std::string tempdir_name = make_temp_dir("/tmp/yosys-qbfsat-XXXXXX"); + RTLIL::Module *module = mod; + RTLIL::Design *design = module->design; + std::string module_name = module->name.str(); + RTLIL::IdString wire_to_optimize_name = ""; + bool maximize = false; + log_assert(module->design != nullptr); + + Pass::call(design, "design -push-copy"); + + //Replace input wires with wires assigned $allconst cells: + pool<std::string> input_wires = validate_design_and_get_inputs(module, opt.assume_outputs); + allconstify_inputs(module, input_wires); + if (opt.assume_outputs) + assume_miter_outputs(module, opt.assume_neg); + + //Find the wire to be optimized, if any: + for (auto wire : module->wires()) { + if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) { + wire_to_optimize_name = wire->name; + maximize = wire->get_bool_attribute("\\maximize"); + if (opt.nooptimize) { + if (maximize) + wire->set_bool_attribute("\\maximize", false); + else + wire->set_bool_attribute("\\minimize", false); + } } } - if(!opt.nocleanup) - remove_directory(tempdir_name); + //If -O1 or -O2 was specified, use ABC to simplify the problem: + if (opt.oflag == opt.OptimizationLevel::O1) + Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;fraig;print_stats;refactor,-N,10,-lz;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str()); + else if (opt.oflag == opt.OptimizationLevel::O2) + Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;dch,-S,1000000,-C,100000,-p;print_stats;fraig;print_stats;refactor,-N,15,-lz;print_stats;dc2,-pbl;print_stats;drwsat;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str()); + if (opt.oflag != opt.OptimizationLevel::O0) { + Pass::call(module->design, "techmap"); + Pass::call(module->design, "opt"); + } - recover_solution(ret); + if (opt.nobisection || opt.nooptimize || wire_to_optimize_name == "") { + ret = call_qbf_solver(module, opt, tempdir_name, false, 0); + } else { + //Do the iterated bisection method: + unsigned int iter_num = 1; + unsigned int success = 0; + unsigned int failure = 0; + unsigned int cur_thresh = 0; + + log_assert(wire_to_optimize_name != ""); + log_assert(module->wire(wire_to_optimize_name) != nullptr); + log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), wire_to_optimize_name.c_str()); + + //If maximizing, grow until we get a failure. Then bisect success and failure. + while (failure == 0 || difference(success, failure) > 1) { + Pass::call(design, "design -push-copy"); + log_header(design, "Preparing QBF-SAT problem.\n"); - return ret; -} + if (cur_thresh != 0) { + //Add thresholding logic (but not on the initial run when we don't have a sense of where to start): + RTLIL::SigSpec comparator = maximize? module->Ge(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false) + : module->Le(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false); -pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { - bool found_input = false; - bool found_hole = false; - bool found_1bit_output = false; - bool found_assert_assume = false; - pool<std::string> input_wires; - for (auto wire : module->wires()) { - if (wire->port_input) { - found_input = true; - input_wires.insert(wire->name.str()); + module->addAssume(wire_to_optimize_name.str() + "__threshold", comparator, RTLIL::Const(1, 1)); + log("Trying to solve with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), cur_thresh); + } + + ret = call_qbf_solver(module, opt, tempdir_name, false, iter_num); + Pass::call(design, "design -pop"); + module = design->module(module_name); + + if (!ret.unknown && ret.sat) { + Pass::call(design, "design -push-copy"); + specialize(module, ret, true); + + RTLIL::SigSpec wire, value, undef; + RTLIL::SigSpec::parse_sel(wire, design, module, wire_to_optimize_name.str()); + + ConstEval ce(module); + value = wire; + if (!ce.eval(value, undef)) + log_cmd_error("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(wire), log_signal(undef)); + log_assert(value.is_fully_const()); + success = value.as_const().as_int(); + best_soln = ret; + log("Problem is satisfiable with %s = %d.\n", wire_to_optimize_name.c_str(), success); + Pass::call(design, "design -pop"); + module = design->module(module_name); + + //sometimes this happens if we get an 'unknown' or timeout + if (!maximize && success < failure) + break; + else if (maximize && failure != 0 && success > failure) + break; + + } else { + //Treat 'unknown' as UNSAT + failure = cur_thresh; + if (failure == 0) { + log("Problem is NOT satisfiable.\n"); + break; + } + else + log("Problem is NOT satisfiable with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), failure); + } + + iter_num++; + if (maximize && failure == 0 && success == 0) + cur_thresh = 2; + else if (maximize && failure == 0) + cur_thresh = 2 * success; //growth + else //if (!maximize || failure != 0) + cur_thresh = (success + failure) / 2; //bisection + } + if (success != 0 || failure != 0) { + log("Wire %s is %s at %d.\n", wire_to_optimize_name.c_str(), (maximize? "maximized" : "minimized"), success); + ret = best_soln; } - if (wire->port_output && wire->width == 1) - found_1bit_output = true; - } - for (auto cell : module->cells()) { - if (cell->type == "$allconst") - found_input = true; - if (cell->type == "$anyconst") - found_hole = true; - if (cell->type.in("$assert", "$assume")) - found_assert_assume = true; } - if (!found_input) - log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n"); - if (!found_hole) - log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); - if (!found_1bit_output && !found_assert_assume) - log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); - if (!found_assert_assume && !opt.assume_outputs) - log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n"); - return input_wires; + if(!opt.nocleanup) + remove_directory(tempdir_name); + + Pass::call(design, "design -pop"); + + return ret; } QbfSolveOptions parse_args(const std::vector<std::string> &args) { @@ -379,6 +395,59 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { opt.assume_neg = true; continue; } + else if (args[opt.argidx] == "-nooptimize") { + opt.nooptimize = true; + continue; + } + else if (args[opt.argidx] == "-nobisection") { + opt.nobisection = true; + continue; + } + else if (args[opt.argidx] == "-solver") { + if (args.size() <= opt.argidx + 1) + log_cmd_error("solver not specified.\n"); + else { + if (args[opt.argidx+1] == "z3") + opt.solver = opt.Solver::Z3; + else if (args[opt.argidx+1] == "yices") + opt.solver = opt.Solver::Yices; + else if (args[opt.argidx+1] == "cvc4") + opt.solver = opt.Solver::CVC4; + else + log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str()); + opt.argidx++; + } + continue; + } + else if (args[opt.argidx] == "-timeout") { + if (args.size() <= opt.argidx + 1) + log_cmd_error("timeout not specified.\n"); + else { + int timeout = atoi(args[opt.argidx+1].c_str()); + if (timeout > 0) + opt.timeout = timeout; + else + log_cmd_error("timeout must be greater than 0.\n"); + opt.argidx++; + } + continue; + } + else if (args[opt.argidx].substr(0, 2) == "-O" && args[opt.argidx].size() == 3) { + switch (args[opt.argidx][2]) { + case '0': + opt.oflag = opt.OptimizationLevel::O0; + break; + case '1': + opt.oflag = opt.OptimizationLevel::O1; + break; + case '2': + opt.oflag = opt.OptimizationLevel::O2; + break; + default: + log_cmd_error("unknown argument %s\n", args[opt.argidx].c_str()); + } + continue; + } else if (args[opt.argidx] == "-sat") { opt.sat = true; continue; @@ -421,62 +490,56 @@ 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() YS_OVERRIDE + void help() 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("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the currently\n"); + log("selected module. Existentially-quantified variables are declared by assigning a wire\n"); + log("\"$anyconst\". Universally-quantified variables may be explicitly declared by assigning\n"); + log("a wire \"$allconst\", but module inputs will be treated as universally-quantified\n"); + log("variables by default.\n"); log("\n"); log(" -nocleanup\n"); - log(" Do not delete temporary files and directories. Useful for\n"); - log(" debugging.\n"); + log(" Do not delete temporary files and directories. Useful for debugging.\n"); log("\n"); log(" -dump-final-smt2 <file>\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(" Add an \"$assume\" cell for the conjunction of all one-bit module output wires.\n"); log("\n"); log(" -assume-negative-polarity\n"); log(" When adding $assume cells for one-bit module output wires, assume they are\n"); log(" negative polarity signals and should always be low, for example like the\n"); log(" miters created with the `miter` command.\n"); log("\n"); + log(" -nooptimize\n"); + log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n"); + log(" \"(minimize)\" in the SMT-LIBv2, and generally make no attempt to optimize anything.\n"); + log("\n"); + log(" -nobisection\n"); + log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n"); + log(" attempt to optimize that value with the default iterated solving and threshold\n"); + log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n"); + log(" command in the SMT-LIBv2 output and hope that the solver supports optimizing\n"); + log(" quantified bitvector problems.\n"); + log("\n"); + log(" -solver <solver>\n"); + log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); + log(" (default: yices)\n"); + log("\n"); + log(" -timeout <value>\n"); + log(" Set the per-iteration timeout in seconds.\n"); + log(" (default: no timeout)\n"); + log("\n"); + log(" -O0, -O1, -O2\n"); + log(" Control the use of ABC to simplify the QBF-SAT problem before solving.\n"); + log("\n"); log(" -sat\n"); log(" Generate an error if the solver does not return \"sat\".\n"); log("\n"); @@ -487,20 +550,21 @@ struct QbfSatPass : public Pass { 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(" If the problem is satisfiable, replace each \"$anyconst\" cell with its\n"); + log(" corresponding constant value from the model produced by the solver.\n"); log("\n"); log(" -specialize-from-file <solution 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(" Do not run the solver, but instead only attempt to replace each \"$anyconst\"\n"); + log(" cell in the current module with a constant value provided by the specified file.\n"); log("\n"); log(" -write-solution <solution file>\n"); - log(" Write the assignments discovered by the solver for all \"$anyconst\" cells\n"); - log(" to the specified file."); + log(" If the problem is satisfiable, write the corresponding constant value for each\n"); + log(" \"$anyconst\" cell from the model produced by the solver to the specified file."); log("\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { log_header(design, "Executing QBFSAT pass (solving QBF-SAT problems in the circuit).\n"); QbfSolveOptions opt = parse_args(args); @@ -519,41 +583,31 @@ struct QbfSatPass : public Pass { if (!opt.specialize_from_file) { //Save the design to restore after modiyfing the current module. std::string module_name = module->name.str(); - Pass::call(design, "design -push-copy"); - - //Replace input wires with wires assigned $allconst cells. - pool<std::string> input_wires = validate_design_and_get_inputs(module, opt); - allconstify_inputs(module, input_wires); - if (opt.assume_outputs) - assume_miter_outputs(module, opt); QbfSolutionType ret = qbf_solve(module, opt); - Pass::call(design, "design -pop"); module = design->module(module_name); - - if (ret.unknown) - log_warning("solver did not give an answer\n"); - else if (ret.sat) + if (ret.unknown) { + if (opt.sat || opt.unsat) + log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); + } + else if (ret.sat) { print_qed(); - else - print_proof_failed(); - - if(!ret.unknown && ret.sat) { if (opt.write_solution) { - write_solution(module, ret, opt.write_soln_soln_file); + 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"); } - else if (!ret.unknown && !ret.sat && opt.sat) - log_cmd_error("expected problem to be SAT\n"); - else if (ret.unknown && (opt.sat || opt.unsat)) - log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); + else { + print_proof_failed(); + if (opt.sat) + log_cmd_error("expected problem to be SAT\n"); + } } else specialize_from_file(module, opt.specialize_soln_file); log_pop(); 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 diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 6acdbc800..d7bf125d1 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -256,13 +256,13 @@ struct SatHelper { RTLIL::SigSpec big_lhs, big_rhs; - for (auto &it : module->wires_) + for (auto wire : module->wires()) { - if (it.second->attributes.count(ID::init) == 0) + if (wire->attributes.count(ID::init) == 0) continue; - RTLIL::SigSpec lhs = sigmap(it.second); - RTLIL::SigSpec rhs = it.second->attributes.at(ID::init); + RTLIL::SigSpec lhs = sigmap(wire); + RTLIL::SigSpec rhs = wire->attributes.at(ID::init); log_assert(lhs.size() == rhs.size()); RTLIL::SigSpec removed_bits; @@ -893,7 +893,7 @@ void print_qed() struct SatPass : public Pass { SatPass() : Pass("sat", "solve a SAT problem in the circuit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -1060,7 +1060,7 @@ struct SatPass : public Pass { log(" Like -falsify but do not return an error for timeouts.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x; std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at; diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 03ca42cf3..fb496ff87 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -163,7 +163,10 @@ struct SimInstance mem_database[cell] = mem; } - + if (cell->type.in(ID($memwr),ID($memrd))) + { + log_error("$memrd and $memwr cells have to be merged to stand-alone $mem cells (execute memory_collect pass)\n"); + } if (cell->type.in(ID($assert), ID($cover), ID($assume))) { formal_database.insert(cell); } @@ -751,7 +754,7 @@ struct SimWorker : SimShared struct SimPass : public Pass { SimPass() : Pass("sim", "simulate the circuit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -793,7 +796,7 @@ struct SimPass : public Pass { log(" enable debug output\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { SimWorker worker; int numcycles = 20; diff --git a/passes/sat/supercover.cc b/passes/sat/supercover.cc index ba44f02d8..aacc044fb 100644 --- a/passes/sat/supercover.cc +++ b/passes/sat/supercover.cc @@ -25,7 +25,7 @@ PRIVATE_NAMESPACE_BEGIN struct SupercoverPass : public Pass { SupercoverPass() : Pass("supercover", "add hi/lo cover cells for each wire bit") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -35,7 +35,7 @@ struct SupercoverPass : public Pass { log("checking for a hi signal level and one checking for lo level.\n"); log("\n"); } - void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::vector<std::string> args, RTLIL::Design *design) override { // bool flag_noinit = false; |