aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat/eval.cc
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat/eval.cc')
-rw-r--r--passes/sat/eval.cc38
1 files changed, 19 insertions, 19 deletions
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 62534ec0b..09f69cc5c 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -2,11 +2,11 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -87,7 +87,7 @@ struct BruteForceEquivChecker
BruteForceEquivChecker(RTLIL::Module *mod1, RTLIL::Module *mod2, bool ignore_x_mod1) :
mod1(mod1), mod2(mod2), counter(0), errors(0), ignore_x_mod1(ignore_x_mod1)
{
- log("Checking for equivialence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str());
+ log("Checking for equivalence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str());
for (auto &w : mod1->wires_)
{
RTLIL::Wire *wire1 = w.second;
@@ -143,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;
@@ -163,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++) {
@@ -204,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.CONST_FALSE : ez.CONST_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));
@@ -220,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");
}
@@ -389,7 +389,7 @@ struct EvalPass : public Pass {
std::vector<std::string> shows, tables;
bool set_undef = false;
- log_header("Executing EVAL pass (evaluate the circuit given an input).\n");
+ log_header(design, "Executing EVAL pass (evaluate the circuit given an input).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@@ -421,7 +421,7 @@ struct EvalPass : public Pass {
log_error("Can't find module `%s'!\n", mod2_name.c_str());
BruteForceEquivChecker checker(design->modules_.at(mod1_name), design->modules_.at(mod2_name), args[argidx-2] == "-brute_force_equiv_checker_x");
if (checker.errors > 0)
- log_cmd_error("Modules are not equivialent!\n");
+ log_cmd_error("Modules are not equivalent!\n");
log("Verified %s = %s (using brute-force check on %d cases).\n",
mod1_name.c_str(), mod2_name.c_str(), checker.counter);
return;
@@ -448,7 +448,7 @@ struct EvalPass : public Pass {
RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
module = mod_it.second;
}
- if (module == NULL)
+ if (module == NULL)
log_cmd_error("Can't perform EVAL on an empty selection!\n");
ConstEval ce(module);
@@ -568,7 +568,7 @@ struct EvalPass : public Pass {
if (tab_column_width.size() < row.size())
tab_column_width.resize(row.size());
for (size_t i = 0; i < row.size(); i++)
- tab_column_width[i] = std::max(tab_column_width[i], int(row[i].size()));
+ tab_column_width[i] = max(tab_column_width[i], int(row[i].size()));
}
log("\n");
@@ -594,10 +594,10 @@ struct EvalPass : public Pass {
log("\n");
if (undef.size() > 0) {
undef.sort_and_unify();
- log("Assumend undef (x) value for the following singals: %s\n\n", log_signal(undef));
+ log("Assumed undef (x) value for the following signals: %s\n\n", log_signal(undef));
}
}
}
} EvalPass;
-
+
PRIVATE_NAMESPACE_END
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-02 17:19:01 +0000