mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 17:15:33 +00:00
Code Activity

Merge branch 'master' of github.com:YosysHQ/yosys into claire/eqystuff

Browse source
This commit is contained in:
Claire Xenia Wolf 2023-01-11 04:10:12 +01:00
commit 6d56d4ecfc
103 changed files with 385 additions and 20236 deletions
Download patch file Download diff file Expand all files Collapse all files

4
passes/cmds/stat.cc
View file

@ -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");

13
passes/cmds/tee.cc
View file

@ -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;

3
passes/sat/formalff.cc
View file

@ -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;

6
passes/sat/qbfsat.cc
View file

@ -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");

4
passes/sat/qbfsat.h
View file

@ -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 "";