diff options
author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-07-01 20:51:14 +0000 |
---|---|---|
committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-07-20 21:54:56 +0000 |
commit | f0379853371bfcf9217c3c0de15b3927b6f09e44 (patch) | |
tree | 42578174b1d80c0bf3c4f356c59119627758bb1f /backends/smt2/smt2.cc | |
parent | 856d40973dce06e13fcded3388562341d82c092d (diff) | |
download | yosys-f0379853371bfcf9217c3c0de15b3927b6f09e44.tar.gz yosys-f0379853371bfcf9217c3c0de15b3927b6f09e44.tar.bz2 yosys-f0379853371bfcf9217c3c0de15b3927b6f09e44.zip |
smt2: Add `-solver-option` option.
Diffstat (limited to 'backends/smt2/smt2.cc')
-rw-r--r-- | backends/smt2/smt2.cc | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 526b36352..a79c0bd99 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1387,6 +1387,10 @@ struct Smt2Backend : public Backend { log(" use the given template file. the line containing only the token '%%%%'\n"); log(" is replaced with the regular output of this command.\n"); log("\n"); + log(" -solver-option <option> <value>\n"); + log(" emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write\n"); + log(" the given option as a `(set-option ...)` command in the SMT-LIBv2.\n"); + log("\n"); log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n"); log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n"); log("\n"); @@ -1441,6 +1445,7 @@ struct Smt2Backend : public Backend { std::ifstream template_f; bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false; bool forallmode = false; + dict<std::string, std::string> solver_options; log_header(design, "Executing SMT2 backend.\n"); @@ -1484,6 +1489,11 @@ struct Smt2Backend : public Backend { verbose = true; continue; } + if (args[argidx] == "-solver-option" && argidx+2 < args.size()) { + solver_options.emplace(args[argidx+1], args[argidx+2]); + argidx += 2; + continue; + } break; } extra_args(f, filename, args, argidx); @@ -1514,6 +1524,9 @@ struct Smt2Backend : public Backend { if (statedt) *f << stringf("; yosys-smt2-stdt\n"); + for (auto &it : solver_options) + *f << stringf("; yosys-smt2-solver-option %s %s\n", it.first.c_str(), it.second.c_str()); + std::vector<RTLIL::Module*> sorted_modules; // extract module dependencies |