diff options
| -rw-r--r-- | backends/smt2/smtio.py | 6 | ||||
| -rw-r--r-- | frontends/ilang/ilang_lexer.l | 4 | ||||
| -rw-r--r-- | frontends/verilog/verilog_lexer.l | 11 | ||||
| -rw-r--r-- | kernel/rtlil.h | 8 | ||||
| -rw-r--r-- | manual/CHAPTER_Overview.tex | 9 | ||||
| -rw-r--r-- | passes/sat/qbfsat.cc | 71 |
6 files changed, 75 insertions, 34 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 69f59df79..62dfe7c11 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -172,7 +172,7 @@ class SmtIo: self.unroll = False if self.solver == "yices": - if self.noincr: + if self.noincr or self.forall: self.popen_vargs = ['yices-smt2'] + self.solver_opts else: self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts @@ -232,12 +232,16 @@ class SmtIo: if self.logic_uf: self.logic += "UF" if self.logic_bv: self.logic += "BV" if self.logic_dt: self.logic = "ALL" + if self.solver == "yices" and self.forall: self.logic = "BV" self.setup_done = True for stmt in self.info_stmts: self.write(stmt) + if self.forall and self.solver == "yices": + self.write("(set-option :yices-ef-max-iters 1000000000)") + if self.produce_models: self.write("(set-option :produce-models true)") diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l index 62f53d18e..3362ed641 100644 --- a/frontends/ilang/ilang_lexer.l +++ b/frontends/ilang/ilang_lexer.l @@ -91,8 +91,10 @@ USING_YOSYS_NAMESPACE [0-9]+'[01xzm-]* { rtlil_frontend_ilang_yylval.string = strdup(yytext); return TOK_VALUE; } -?[0-9]+ { char *end = nullptr; + errno = 0; long value = strtol(yytext, &end, 10); - if (end != yytext + strlen(yytext)) + log_assert(end == yytext + strlen(yytext)); + if (errno == ERANGE) return TOK_INVALID; // literal out of range of long if (value < INT_MIN || value > INT_MAX) return TOK_INVALID; // literal out of range of int (relevant mostly for LP64 platforms) diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 65a2e9a78..02fa0031b 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -48,16 +48,18 @@ USING_YOSYS_NAMESPACE using namespace AST; using namespace VERILOG_FRONTEND; +#define YYSTYPE FRONTEND_VERILOG_YYSTYPE +#define YYLTYPE FRONTEND_VERILOG_YYLTYPE + YOSYS_NAMESPACE_BEGIN namespace VERILOG_FRONTEND { std::vector<std::string> fn_stack; std::vector<int> ln_stack; + YYLTYPE real_location; + YYLTYPE old_location; } YOSYS_NAMESPACE_END -#define YYSTYPE FRONTEND_VERILOG_YYSTYPE -#define YYLTYPE FRONTEND_VERILOG_YYLTYPE - #define SV_KEYWORD(_tok) \ if (sv_mode) return _tok; \ log("Lexer warning: The SystemVerilog keyword `%s' (at %s:%d) is not "\ @@ -73,9 +75,6 @@ YOSYS_NAMESPACE_END #define YY_INPUT(buf,result,max_size) \ result = readsome(*VERILOG_FRONTEND::lexin, buf, max_size) -YYLTYPE real_location; -YYLTYPE old_location; - #define YY_USER_ACTION \ old_location = real_location; \ real_location.first_line = real_location.last_line; \ diff --git a/kernel/rtlil.h b/kernel/rtlil.h index a418c9996..8228523d5 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -150,9 +150,6 @@ namespace RTLIL if (!p[0]) return 0; - log_assert(p[0] == '$' || p[0] == '\\'); - log_assert(p[1] != 0); - auto it = global_id_index_.find((char*)p); if (it != global_id_index_.end()) { #ifndef YOSYS_NO_IDS_REFCNT @@ -165,6 +162,11 @@ namespace RTLIL return it->second; } + log_assert(p[0] == '$' || p[0] == '\\'); + log_assert(p[1] != 0); + for (const char *c = p; *c; c++) + log_assert((unsigned)*c > (unsigned)' '); + #ifndef YOSYS_NO_IDS_REFCNT if (global_free_idx_list_.empty()) { if (global_id_storage_.empty()) { diff --git a/manual/CHAPTER_Overview.tex b/manual/CHAPTER_Overview.tex index be37d8d39..ac0f48e47 100644 --- a/manual/CHAPTER_Overview.tex +++ b/manual/CHAPTER_Overview.tex @@ -184,9 +184,12 @@ may hold important information for Yosys developers can be used without disturbing external tools. For example the Verilog backend assigns names in the form {\tt \_{\it integer}\_}. \end{itemize} -In order to avoid programming errors, the RTLIL data structures check if all -identifiers start with either a backslash or a dollar sign and generate a -runtime error if this rule is violated. +Whitespace and control characters (any character with an ASCII code 32 or less) are not allowed +in RTLIL identifiers; most frontends and backends cannot support these characters in identifiers. + +In order to avoid programming errors, the RTLIL data structures check if all identifiers start +with either a backslash or a dollar sign, and contain no whitespace or control characters. +Violating these rules results in a runtime error. All RTLIL identifiers are case sensitive. diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index c42760488..712a46cbc 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -41,6 +41,7 @@ struct QbfSolveOptions { bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg; bool nooptimize, nobisection; bool sat, unsat, show_smtbmc; + enum Solver{Z3, Yices, CVC4} solver; std::string specialize_soln_file; std::string write_soln_soln_file; std::string dump_final_smt2_file; @@ -48,9 +49,21 @@ struct QbfSolveOptions { QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false), nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false), - argidx(0) {}; + solver(Yices), argidx(0) {}; }; +std::string get_solver_name(const QbfSolveOptions &opt) { + if (opt.solver == opt.Solver::Z3) + return "z3"; + else if (opt.solver == opt.Solver::Yices) + return "yices"; + else if (opt.solver == opt.Solver::CVC4) + return "cvc4"; + else + log_cmd_error("unknown solver specified.\n"); + return ""; +} + 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"); @@ -315,19 +328,18 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2"; - const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1"; const std::string smtbmc_warning = "z3: WARNING:"; - const bool show_smtbmc = opt.show_smtbmc; + const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1"; Pass::call(mod->design, smt2_command); - auto process_line = [&ret, &smtbmc_warning, &show_smtbmc, &quiet](const std::string &line) { + 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 (show_smtbmc && !quiet) + if (opt.show_smtbmc && !quiet) log("smtbmc output: %s", line.c_str()); }; log_header(mod->design, "Solving QBF-SAT problem.\n"); @@ -486,6 +498,22 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { 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] == "-sat") { opt.sat = true; continue; @@ -563,21 +591,20 @@ struct QbfSatPass : public Pass { 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"); @@ -586,15 +613,18 @@ struct QbfSatPass : public Pass { log("\n"); log(" -nooptimize\n"); log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n"); - log(" \"(minimize)\" in the SMTLIBv2, and generally make no attempt to optimize anything.\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 SMTLIBv2 output and hope that the solver supports optimizing\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("\n"); log(" -sat\n"); log(" Generate an error if the solver does not return \"sat\".\n"); log("\n"); @@ -605,15 +635,16 @@ 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"); } |