diff options
author | Claire Xenia Wolf <claire@clairexen.net> | 2023-01-11 04:10:12 +0100 |
---|---|---|
committer | Claire Xenia Wolf <claire@clairexen.net> | 2023-01-11 04:10:12 +0100 |
commit | 6d56d4ecfc2c9afda3fd58f945a5f10daf87a999 (patch) | |
tree | 8b2e2cd5018674f287ae8b2c20877615fec8b555 /passes | |
parent | 029b0aac7f10ff5e1d927fb6ec1d9571a5350176 (diff) | |
parent | 7b476996df962b63656152f643ff2181143f516e (diff) | |
download | yosys-6d56d4ecfc2c9afda3fd58f945a5f10daf87a999.tar.gz yosys-6d56d4ecfc2c9afda3fd58f945a5f10daf87a999.tar.bz2 yosys-6d56d4ecfc2c9afda3fd58f945a5f10daf87a999.zip |
Merge branch 'master' of github.com:YosysHQ/yosys into claire/eqystuff
Diffstat (limited to 'passes')
-rw-r--r-- | passes/cmds/stat.cc | 4 | ||||
-rw-r--r-- | passes/cmds/tee.cc | 13 | ||||
-rw-r--r-- | passes/sat/formalff.cc | 3 | ||||
-rw-r--r-- | passes/sat/qbfsat.cc | 6 | ||||
-rw-r--r-- | passes/sat/qbfsat.h | 4 |
5 files changed, 25 insertions, 5 deletions
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index a998ab8e7..10e98952e 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -452,7 +452,7 @@ struct StatPass : public Pass { if (json_mode) { log("\n"); - log(" },\n"); + log(top_mod == nullptr ? " }\n" : " },\n"); } if (top_mod != nullptr) @@ -466,7 +466,7 @@ struct StatPass : public Pass { statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0, /*quiet=*/json_mode); - if (json_mode) + if (json_mode) data.log_data_json("design", true); else if (GetSize(mod_stat) > 1) { log("\n"); diff --git a/passes/cmds/tee.cc b/passes/cmds/tee.cc index 7a1f4a36b..39ed4a7a8 100644 --- a/passes/cmds/tee.cc +++ b/passes/cmds/tee.cc @@ -45,6 +45,9 @@ struct TeePass : public Pass { log(" -a logfile\n"); log(" Write output to this file, append if exists.\n"); log("\n"); + log(" -s scratchpad\n"); + log(" Write output to this scratchpad value, truncate if it exists.\n"); + log("\n"); log(" +INT, -INT\n"); log(" Add/subtract INT from the -v setting for this command.\n"); log("\n"); @@ -53,9 +56,11 @@ struct TeePass : public Pass { { std::vector<FILE*> backup_log_files, files_to_close; std::vector<std::ostream*> backup_log_streams; + std::vector<std::string> backup_log_scratchpads; int backup_log_verbose_level = log_verbose_level; backup_log_streams = log_streams; backup_log_files = log_files; + backup_log_scratchpads = log_scratchpads; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) @@ -78,6 +83,12 @@ struct TeePass : public Pass { files_to_close.push_back(f); continue; } + if (args[argidx] == "-s" && argidx+1 < args.size()) { + auto name = args[++argidx]; + design->scratchpad[name] = ""; + log_scratchpads.push_back(name); + continue; + } if (GetSize(args[argidx]) >= 2 && (args[argidx][0] == '-' || args[argidx][0] == '+') && args[argidx][1] >= '0' && args[argidx][1] <= '9') { log_verbose_level += atoi(args[argidx].c_str()); continue; @@ -93,6 +104,7 @@ struct TeePass : public Pass { fclose(cf); log_files = backup_log_files; log_streams = backup_log_streams; + log_scratchpads = backup_log_scratchpads; throw; } @@ -102,6 +114,7 @@ struct TeePass : public Pass { log_verbose_level = backup_log_verbose_level; log_files = backup_log_files; log_streams = backup_log_streams; + log_scratchpads = backup_log_scratchpads; } } TeePass; diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index b2a91b155..e36379096 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -479,6 +479,9 @@ struct FormalFfPass : public Pass { if (ff.sig_clk.is_fully_const()) log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", log_id(cell), log_id(cell->type), log_id(module)); + if (ff.has_aload || ff.has_arst || ff.has_sr) + log_error("Async inputs on %s (%s) from module %s, run async2sync first.\n", + log_id(cell), log_id(cell->type), log_id(module)); auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr; diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 4580f194e..42d3e188a 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -416,6 +416,8 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { opt.solver = opt.Solver::Yices; else if (args[opt.argidx+1] == "cvc4") opt.solver = opt.Solver::CVC4; + else if (args[opt.argidx+1] == "cvc5") + opt.solver = opt.Solver::CVC5; else log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str()); opt.argidx++; @@ -542,8 +544,8 @@ struct QbfSatPass : public Pass { log(" hope that the solver supports optimizing quantified bitvector problems.\n"); log("\n"); log(" -solver <solver>\n"); - log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); - log(" (default: yices)\n"); + log(" Use a particular solver. Choose one of: \"z3\", \"yices\", \"cvc4\"\n"); + log(" and \"cvc5\". (default: yices)\n"); log("\n"); log(" -solver-option <name> <value>\n"); log(" Set the specified solver option in the SMT-LIBv2 problem file.\n"); diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h index c96c6f818..8fb6093bc 100644 --- a/passes/sat/qbfsat.h +++ b/passes/sat/qbfsat.h @@ -29,7 +29,7 @@ struct QbfSolveOptions { bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false; bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false; bool nobisection = false, sat = false, unsat = false, show_smtbmc = false; - enum Solver{Z3, Yices, CVC4} solver = Yices; + enum Solver{Z3, Yices, CVC4, CVC5} solver = Yices; enum OptimizationLevel{O0, O1, O2} oflag = O0; dict<std::string, std::string> solver_options; int timeout = 0; @@ -45,6 +45,8 @@ struct QbfSolveOptions { return "yices"; else if (solver == Solver::CVC4) return "cvc4"; + else if (solver == Solver::CVC5) + return "cvc5"; log_cmd_error("unknown solver specified.\n"); return ""; |