riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole value recovery using that mode.

This commit is contained in:
Alberto Gonzalez 2020-03-25 23:17:50 +00:00
parent a4598d64ef
commit 437afa1f0c
No known key found for this signature in database
GPG Key ID: 8395A8BA109708B2
2 changed files with 54 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
backends/smt2/smtbmc.py
View File

@ -49,6 +49,7 @@ presat = False
smtcinit = False smtcinit = False
smtctop = None smtctop = None
noinit = False noinit = False
binarymode = False
so = SmtOpts() so = SmtOpts()
@ -150,6 +151,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
add <num_steps> time steps at the end of the trace add <num_steps> time steps at the end of the trace
when creating a counter example (this additional time when creating a counter example (this additional time
steps will still be constrained by assumptions) steps will still be constrained by assumptions)
--binary
dump anyconst values as raw bit strings
""" + so.helpmsg()) """ + so.helpmsg())
sys.exit(1) sys.exit(1)
@ -158,7 +162,7 @@ try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat", ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
"dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
"smtc-init", "smtc-top=", "noinit"]) "smtc-init", "smtc-top=", "noinit", "binary"])
except: except:
usage() usage()
@ -229,6 +233,8 @@ for o, a in opts:
covermode = True covermode = True
elif o == "-m": elif o == "-m":
topmod = a topmod = a
elif o == "--binary":
binarymode = True
elif so.handle(o, a): elif so.handle(o, a):
pass pass
else: else:
@ -1089,9 +1095,15 @@ def print_anyconsts_worker(mod, state, path):
for fun, info in smt.modinfo[mod].anyconsts.items(): for fun, info in smt.modinfo[mod].anyconsts.items():
if info[1] is None: 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: 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): def print_anyconsts(state):

68
passes/sat/qbfsat.cc
View File

@ -23,6 +23,7 @@
#include "kernel/rtlil.h" #include "kernel/rtlil.h"
#include "kernel/register.h" #include "kernel/register.h"
#include <cstdio> #include <cstdio>
#include <algorithm>
#if defined(_WIN32) #if defined(_WIN32)
# define WIFEXITED(x) 1 # define WIFEXITED(x) 1
@ -57,7 +58,7 @@ struct QbfSolveOptions {
nocleanup(false), dump_final_smt2(false), timeout_sec(-1) {}; 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 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_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); YS_REGEX_TYPE hole_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); 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 qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
QbfSolutionType ret; QbfSolutionType ret;
std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; 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); log_assert(mod->design != nullptr);
Pass::call(mod->design, smt2_command); 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); fflush(stdout);
bool keep_reading = true; bool keep_reading = true;
@ -103,7 +137,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
int retval = 0; int retval = 0;
char buf[1024] = {0}; char buf[1024] = {0};
std::string linebuf = ""; 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()); log("Launching \"%s\".\n", cmd.c_str());
#ifndef EMSCRIPTEN #ifndef EMSCRIPTEN
@ -154,7 +188,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
if(!opt.nocleanup) if(!opt.nocleanup)
remove_directory(tempdir_name); remove_directory(tempdir_name);
recover_solution(mod, ret); recover_solution(ret);
return ret; return ret;
} }
@ -341,31 +375,7 @@ struct QbfSatPass : public Pass {
print_proof_failed(); print_proof_failed();
if (opt.specialize) { if (opt.specialize) {
std::map<std::string, std::string> hole_loc_to_name; specialize(module, ret);
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);
}
Pass::call(design, "opt_clean"); Pass::call(design, "opt_clean");
} }
} }