aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/exec.cc8
-rw-r--r--passes/cmds/logger.cc8
-rw-r--r--passes/cmds/stat.cc4
-rw-r--r--passes/cmds/tee.cc13
-rw-r--r--passes/sat/formalff.cc3
-rw-r--r--passes/sat/qbfsat.cc16
-rw-r--r--passes/sat/qbfsat.h50
7 files changed, 61 insertions, 41 deletions
diff --git a/passes/cmds/exec.cc b/passes/cmds/exec.cc
index c15ef23bf..e5fa4fb41 100644
--- a/passes/cmds/exec.cc
+++ b/passes/cmds/exec.cc
@@ -86,7 +86,7 @@ struct ExecPass : public Pass {
bool polarity; //true: this regex must match at least one line
//false: this regex must not match any line
std::string str;
- YS_REGEX_TYPE re;
+ std::regex re;
expect_stdout_elem() : matched(false), polarity(true), str(), re(){};
};
@@ -121,7 +121,7 @@ struct ExecPass : public Pass {
x.str = args[argidx];
x.re = YS_REGEX_COMPILE(args[argidx]);
expect_stdout.push_back(x);
- } catch (const YS_REGEX_NS::regex_error& e) {
+ } catch (const std::regex_error& e) {
log_cmd_error("Error in regex expression '%s' !\n", args[argidx].c_str());
}
} else if (args[argidx] == "-not-expect-stdout") {
@@ -136,7 +136,7 @@ struct ExecPass : public Pass {
x.re = YS_REGEX_COMPILE(args[argidx]);
x.polarity = false;
expect_stdout.push_back(x);
- } catch (const YS_REGEX_NS::regex_error& e) {
+ } catch (const std::regex_error& e) {
log_cmd_error("Error in regex expression '%s' !\n", args[argidx].c_str());
}
@@ -171,7 +171,7 @@ struct ExecPass : public Pass {
if (flag_expect_stdout)
for(auto &x : expect_stdout)
- if (YS_REGEX_NS::regex_search(line, x.re))
+ if (std::regex_search(line, x.re))
x.matched = true;
pos = linebuf.find('\n');
diff --git a/passes/cmds/logger.cc b/passes/cmds/logger.cc
index ec92f1d01..9e45e86af 100644
--- a/passes/cmds/logger.cc
+++ b/passes/cmds/logger.cc
@@ -104,7 +104,7 @@ struct LoggerPass : public Pass {
log("Added regex '%s' for warnings to warn list.\n", pattern.c_str());
log_warn_regexes.push_back(YS_REGEX_COMPILE(pattern));
}
- catch (const YS_REGEX_NS::regex_error& e) {
+ catch (const std::regex_error& e) {
log_cmd_error("Error in regex expression '%s' !\n", pattern.c_str());
}
continue;
@@ -116,7 +116,7 @@ struct LoggerPass : public Pass {
log("Added regex '%s' for warnings to nowarn list.\n", pattern.c_str());
log_nowarn_regexes.push_back(YS_REGEX_COMPILE(pattern));
}
- catch (const YS_REGEX_NS::regex_error& e) {
+ catch (const std::regex_error& e) {
log_cmd_error("Error in regex expression '%s' !\n", pattern.c_str());
}
continue;
@@ -128,7 +128,7 @@ struct LoggerPass : public Pass {
log("Added regex '%s' for warnings to werror list.\n", pattern.c_str());
log_werror_regexes.push_back(YS_REGEX_COMPILE(pattern));
}
- catch (const YS_REGEX_NS::regex_error& e) {
+ catch (const std::regex_error& e) {
log_cmd_error("Error in regex expression '%s' !\n", pattern.c_str());
}
continue;
@@ -172,7 +172,7 @@ struct LoggerPass : public Pass {
log_expect_log[pattern] = LogExpectedItem(YS_REGEX_COMPILE(pattern), count);
else log_abort();
}
- catch (const YS_REGEX_NS::regex_error& e) {
+ catch (const std::regex_error& e) {
log_cmd_error("Error in regex expression '%s' !\n", pattern.c_str());
}
continue;
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..db6836ea1 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -66,9 +66,9 @@ pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, bool ass
}
void specialize_from_file(RTLIL::Module *module, const std::string &file) {
- YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$");
- YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified
- YS_REGEX_MATCH_TYPE bit_m, m;
+ std::regex hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$");
+ std::regex hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified
+ std::smatch bit_m, m;
dict<pool<std::string>, RTLIL::Cell*> anyconst_loc_to_cell;
dict<RTLIL::SigBit, RTLIL::State> hole_assignments;
@@ -83,9 +83,9 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) {
std::string buf;
while (std::getline(fin, buf)) {
bool bit_assn = true;
- if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) {
+ if (!std::regex_search(buf, bit_m, hole_bit_assn_regex)) {
bit_assn = false;
- if (!YS_REGEX_NS::regex_search(buf, m, hole_assn_regex))
+ if (!std::regex_search(buf, m, hole_assn_regex))
log_cmd_error("solution file is not formatted correctly: \"%s\"\n", buf.c_str());
}
@@ -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..253cecce4 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 "";
@@ -152,67 +154,67 @@ struct QbfSolutionType {
}
void recover_solution() {
- 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_regex2 = YS_REGEX_COMPILE("Status: FAILED");
- YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
- YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
- YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
- YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
- YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
- YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
+ std::regex sat_regex = YS_REGEX_COMPILE("Status: PASSED");
+ std::regex unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
+ std::regex unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
+ std::regex timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
+ std::regex timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
+ std::regex unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
+ std::regex unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
+ std::regex memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
+ std::regex hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
#ifndef NDEBUG
- YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
- YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
+ std::regex hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
+ std::regex hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
#endif
- YS_REGEX_MATCH_TYPE m;
+ std::smatch m;
bool sat_regex_found = false;
bool unsat_regex_found = false;
dict<std::string, bool> hole_value_recovered;
for (const std::string &x : stdout_lines) {
- if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
+ if(std::regex_search(x, m, hole_value_regex)) {
std::string loc = m[1].str();
std::string val = m[2].str();
#ifndef NDEBUG
- log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
- log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
+ log_assert(std::regex_search(loc, hole_loc_regex));
+ log_assert(std::regex_search(val, hole_val_regex));
#endif
auto locs = split_tokens(loc, "|");
pool<std::string> loc_pool(locs.begin(), locs.end());
hole_to_value[loc_pool] = val;
}
- else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
+ else if (std::regex_search(x, sat_regex)) {
sat_regex_found = true;
sat = true;
unknown = false;
}
- else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
+ else if (std::regex_search(x, unsat_regex)) {
unsat_regex_found = true;
sat = false;
unknown = false;
}
- else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
+ else if (std::regex_search(x, memout_regex)) {
unknown = true;
log_warning("solver ran out of memory\n");
}
- else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
+ else if (std::regex_search(x, timeout_regex)) {
unknown = true;
log_warning("solver timed out\n");
}
- else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
+ else if (std::regex_search(x, timeout_regex2)) {
unknown = true;
log_warning("solver timed out\n");
}
- else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
+ else if (std::regex_search(x, unknown_regex)) {
unknown = true;
log_warning("solver returned \"unknown\"\n");
}
- else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
+ else if (std::regex_search(x, unsat_regex2)) {
unsat_regex_found = true;
sat = false;
unknown = false;
}
- else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
+ else if (std::regex_search(x, unknown_regex2)) {
unknown = true;
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-14 22:55:59 +0000