aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/formalff.cc2
-rw-r--r--passes/sat/miter.cc24
-rw-r--r--passes/sat/qbfsat.cc16
-rw-r--r--passes/sat/qbfsat.h50
-rw-r--r--passes/sat/sim.cc36
5 files changed, 79 insertions, 49 deletions
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index 962e350a1..e36379096 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -532,12 +532,14 @@ struct FormalFfPass : public Pass {
if ((int)bits.size() == ff.val_init.size()) {
// This check is only to make the private names more helpful for debugging
ff.is_anyinit = true;
+ ff.is_fine = false;
emit = true;
break;
}
auto slice = ff.slice(bits);
slice.is_anyinit = is_anyinit;
+ slice.is_fine = false;
slice.emit();
}
}
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index bf33c9ce3..8f27c4c6f 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -30,6 +30,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
bool flag_make_outputs = false;
bool flag_make_outcmp = false;
bool flag_make_assert = false;
+ bool flag_make_cover = false;
bool flag_flatten = false;
bool flag_cross = false;
@@ -54,6 +55,10 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
flag_make_assert = true;
continue;
}
+ if (args[argidx] == "-make_cover") {
+ flag_make_cover = true;
+ continue;
+ }
if (args[argidx] == "-flatten") {
flag_flatten = true;
continue;
@@ -139,8 +144,16 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
{
if (gold_cross_ports.count(gold_wire))
{
- RTLIL::Wire *w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
+ SigSpec w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width);
gold_cell->setPort(gold_wire->name, w);
+ if (flag_ignore_gold_x) {
+ RTLIL::SigSpec w_x = miter_module->addWire(NEW_ID, GetSize(w));
+ for (int i = 0; i < GetSize(w); i++)
+ miter_module->addEqx(NEW_ID, w[i], State::Sx, w_x[i]);
+ RTLIL::SigSpec w_any = miter_module->And(NEW_ID, miter_module->Anyseq(NEW_ID, GetSize(w)), w_x);
+ RTLIL::SigSpec w_masked = miter_module->And(NEW_ID, w, miter_module->Not(NEW_ID, w_x));
+ w = miter_module->And(NEW_ID, w_any, w_masked);
+ }
gate_cell->setPort(gold_wire->name, w);
continue;
}
@@ -237,6 +250,12 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
}
+ if (flag_make_cover)
+ {
+ auto cover_condition = miter_module->Not(NEW_ID, this_condition);
+ miter_module->addCover("\\cover_" + RTLIL::unescape_id(gold_wire->name), cover_condition, State::S1);
+ }
+
all_conditions.append(this_condition);
}
}
@@ -402,6 +421,9 @@ struct MiterPass : public Pass {
log(" -make_assert\n");
log(" also create an 'assert' cell that checks if trigger is always low.\n");
log("\n");
+ log(" -make_cover\n");
+ log(" also create a 'cover' cell for each gold/gate output pair.\n");
+ log("\n");
log(" -flatten\n");
log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n");
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;
}
}
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 1cd1ebc71..0084a1f28 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -509,7 +509,7 @@ struct SimInstance
}
}
- bool update_ph2()
+ bool update_ph2(bool gclk)
{
bool did_something = false;
@@ -567,7 +567,8 @@ struct SimInstance
}
if (ff_data.has_gclk) {
// $ff
- current_q = ff.past_d;
+ if (gclk)
+ current_q = ff.past_d;
}
if (set_state(ff_data.sig_q, current_q))
did_something = true;
@@ -616,7 +617,7 @@ struct SimInstance
}
for (auto it : children)
- if (it.second->update_ph2()) {
+ if (it.second->update_ph2(gclk)) {
dirty_children.insert(it.second);
did_something = true;
}
@@ -684,10 +685,11 @@ struct SimInstance
void writeback(pool<Module*> &wbmods)
{
- if (wbmods.count(module))
- log_error("Instance %s of module %s is not unique: Writeback not possible. (Fix by running 'uniquify'.)\n", hiername().c_str(), log_id(module));
-
- wbmods.insert(module);
+ if (!ff_database.empty() || !mem_database.empty()) {
+ if (wbmods.count(module))
+ log_error("Instance %s of module %s is not unique: Writeback not possible. (Fix by running 'uniquify'.)\n", hiername().c_str(), log_id(module));
+ wbmods.insert(module);
+ }
for (auto wire : module->wires())
wire->attributes.erase(ID::init);
@@ -985,7 +987,7 @@ struct SimWorker : SimShared
writer->write(use_signal);
}
- void update()
+ void update(bool gclk)
{
while (1)
{
@@ -997,7 +999,7 @@ struct SimWorker : SimShared
if (debug)
log("\n-- ph2 --\n");
- if (!top->update_ph2())
+ if (!top->update_ph2(gclk))
break;
}
@@ -1047,7 +1049,7 @@ struct SimWorker : SimShared
set_inports(clock, State::Sx);
set_inports(clockn, State::Sx);
- update();
+ update(false);
register_output_step(0);
@@ -1060,7 +1062,7 @@ struct SimWorker : SimShared
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
- update();
+ update(true);
register_output_step(10*cycle + 5);
if (debug)
@@ -1076,7 +1078,7 @@ struct SimWorker : SimShared
set_inports(resetn, State::S1);
}
- update();
+ update(true);
register_output_step(10*cycle + 10);
}
@@ -1193,7 +1195,7 @@ struct SimWorker : SimShared
initial = false;
}
if (did_something)
- update();
+ update(true);
register_output_step(time);
bool status = top->checkSignals();
@@ -1342,12 +1344,12 @@ struct SimWorker : SimShared
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
}
- update();
+ update(true);
register_output_step(10*cycle);
if (!multiclock && cycle) {
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
- update();
+ update(true);
register_output_step(10*cycle + 5);
}
cycle++;
@@ -1419,12 +1421,12 @@ struct SimWorker : SimShared
log("Simulating cycle %d.\n", cycle);
set_inports(clock, State::S1);
set_inports(clockn, State::S0);
- update();
+ update(true);
register_output_step(10*cycle+0);
if (!multiclock) {
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
- update();
+ update(true);
register_output_step(10*cycle+5);
}
cycle++;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-04 16:27:07 +0000