mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-07 19:51:23 +00:00
Code Activity

Merge branch 'master' into claire/eqystuff

Browse source
This commit is contained in:
Claire Xen 2023-01-11 16:33:08 +01:00 • committed by GitHub
commit 843f329b96
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
12 changed files with 60 additions and 131 deletions
Download patch file Download diff file Expand all files Collapse all files

10
passes/sat/qbfsat.cc
View file

@ -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());
}

46
passes/sat/qbfsat.h
View file

@ -154,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;
}
}