Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole value recov...

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 63046441960db76e5453e0304354b301477c5ec7..4af4c8ae02ab83c3269fc9591aec6e967d2b8556 100644 (file)
--- 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] <yosys_smt2_output>
         add <num_steps> 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 3045c228401e4a5a1cab54bed1998a5afb65dcc9..cab6f53f37b72fa04a2e7d2835816e4de3093dd9 100644 (file)
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -23,6 +23,7 @@
 #include "kernel/rtlil.h"
 #include "kernel/register.h"
 #include <cstdio>
+#include <algorithm>
 
 #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<std::string, std::string> 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<RTLIL::SigBit> 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 <file>]`
+       //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
        {
                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<std::string, std::string> 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");
                }
        }