diff options
Diffstat (limited to 'passes/sat/eval.cc')
| -rw-r--r-- | passes/sat/eval.cc | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index f07ad943c..01d0e031c 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -31,7 +31,8 @@ #include <string.h> #include <algorithm> -namespace { +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN /* this should only be used for regression testing of ConstEval -- see vloghammer */ struct BruteForceEquivChecker @@ -68,7 +69,7 @@ struct BruteForceEquivChecker log_signal(undef2), log_signal(mod1_inputs), log_signal(inputs)); if (ignore_x_mod1) { - for (int i = 0; i < SIZE(sig1); i++) + for (int i = 0; i < GetSize(sig1); i++) if (sig1[i] == RTLIL::State::Sx) sig2[i] = RTLIL::State::Sx; } @@ -142,16 +143,16 @@ struct VlogHammerReporter { log("Verifying SAT model (%s)..\n", model_undef ? "with undef" : "without undef"); - ezDefaultSAT ez; + ezSatPtr ez; SigMap sigmap(module); - SatGen satgen(&ez, &sigmap); + SatGen satgen(ez.get(), &sigmap); satgen.model_undef = model_undef; for (auto &c : module->cells_) if (!satgen.importCell(c.second)) log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type)); - ez.assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals)); + ez->assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals)); std::vector<int> y_vec = satgen.importDefSigSpec(module->wires_.at("\\y")); std::vector<bool> y_values; @@ -162,9 +163,9 @@ struct VlogHammerReporter } log(" Created SAT problem with %d variables and %d clauses.\n", - ez.numCnfVariables(), ez.numCnfClauses()); + ez->numCnfVariables(), ez->numCnfClauses()); - if (!ez.solve(y_vec, y_values)) + if (!ez->solve(y_vec, y_values)) log_error("Failed to find solution to SAT problem.\n"); for (int i = 0; i < expected_y.size(); i++) { @@ -203,7 +204,7 @@ struct VlogHammerReporter if (y_undef.at(i)) { log(" Toggling undef bit %d to test undef gating.\n", i); - if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.FALSE : ez.TRUE))) + if (!ez->solve(y_vec, y_values, ez->IFF(y_vec.at(i), y_values.at(i) ? ez->CONST_FALSE : ez->CONST_TRUE))) log_error("Failed to find solution with toggled bit!\n"); cmp_vars.push_back(y_vec.at(expected_y.size() + i)); @@ -219,15 +220,15 @@ struct VlogHammerReporter } log(" Testing if SAT solution is unique.\n"); - ez.assume(ez.vec_ne(cmp_vars, ez.vec_const(cmp_vals))); - if (ez.solve(y_vec, y_values)) + ez->assume(ez->vec_ne(cmp_vars, ez->vec_const(cmp_vals))); + if (ez->solve(y_vec, y_values)) log_error("Found two distinct solutions to SAT problem.\n"); } else { log(" Testing if SAT solution is unique.\n"); - ez.assume(ez.vec_ne(y_vec, ez.vec_const(y_values))); - if (ez.solve(y_vec, y_values)) + ez->assume(ez->vec_ne(y_vec, ez->vec_const(y_values))); + if (ez->solve(y_vec, y_values)) log_error("Found two distinct solutions to SAT problem.\n"); } @@ -276,7 +277,7 @@ struct VlogHammerReporter while (!ce.eval(sig, undef)) { // log_error("Evaluation of y in module %s failed: sig=%s, undef=%s\n", RTLIL::id2cstr(module->name), log_signal(sig), log_signal(undef)); - log("Warning: Setting signal %s in module %s to undef.\n", log_signal(undef), RTLIL::id2cstr(module->name)); + log_warning("Setting signal %s in module %s to undef.\n", log_signal(undef), RTLIL::id2cstr(module->name)); ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.size())); } @@ -289,7 +290,7 @@ struct VlogHammerReporter } else if (rtl_sig.size() > 0) { if (rtl_sig.size() != sig.size()) log_error("Output (y) has a different width in module %s compared to rtl!\n", RTLIL::id2cstr(module->name)); - for (int i = 0; i < SIZE(sig); i++) + for (int i = 0; i < GetSize(sig); i++) if (rtl_sig[i] == RTLIL::State::Sx) sig[i] = RTLIL::State::Sx; } @@ -357,8 +358,6 @@ struct VlogHammerReporter } }; -} /* namespace */ - struct EvalPass : public Pass { EvalPass() : Pass("eval", "evaluate the circuit given an input") { } virtual void help() @@ -601,3 +600,4 @@ struct EvalPass : public Pass { } } EvalPass; +PRIVATE_NAMESPACE_END |