From 437afa1f0cbc6534dbb7ec9a4024276e75afce01 Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 25 Mar 2020 23:17:50 +0000 Subject: [PATCH] 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"); } }