summaryrefslogtreecommitdiff
path: root/passes/sat/eval.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-11-25 16:50:45 +0100
committerClifford Wolf <clifford@clifford.at>2013-11-25 16:50:45 +0100
commit61412d167f7bfbdb407a772301665a4c6f5f2240 (patch)
tree5a617c45a482e156e3824a38b64bc0897a29624a /passes/sat/eval.cc
parentbd65e67d8a0ecc71ae0b5df56799e25dd5f2d99a (diff)
Improvements in satgen undef handling
Diffstat (limited to 'passes/sat/eval.cc')
-rw-r--r--passes/sat/eval.cc53
1 files changed, 39 insertions, 14 deletions
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 98e23598..85a136cb 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -155,18 +155,9 @@ struct VlogHammerReporter
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));
- std::vector<int> rec_var_vec = satgen.importSigSpec(recorded_set_vars);
- std::vector<int> rec_val_vec = satgen.importSigSpec(recorded_set_vals);
- ez.assume(ez.vec_eq(rec_var_vec, rec_val_vec));
+ ez.assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals));
- std::vector<int> rec_undef_var_vec, rec_undef_val_vec;
- if (model_undef) {
- rec_undef_var_vec = satgen.importUndefSigSpec(recorded_set_vars);
- rec_undef_val_vec = satgen.importUndefSigSpec(recorded_set_vals);
- ez.assume(ez.vec_eq(rec_undef_var_vec, rec_undef_val_vec));
- }
-
- std::vector<int> y_vec = satgen.importSigSpec(module->wires.at("\\y"));
+ std::vector<int> y_vec = satgen.importDefSigSpec(module->wires.at("\\y"));
std::vector<bool> y_values;
if (model_undef) {
@@ -207,10 +198,44 @@ struct VlogHammerReporter
}
}
- ez.assume(ez.vec_ne(y_vec, ez.vec_const(y_values)));
+ if (model_undef)
+ {
+ std::vector<int> cmp_vars;
+ std::vector<bool> cmp_vals;
- if (ez.solve(y_vec, y_values))
- log_error("Found two distinct solutions to SAT problem.\n");
+ std::vector<bool> y_undef(y_values.begin() + expected_y.width, y_values.end());
+
+ for (int i = 0; i < expected_y.width; i++)
+ 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)))
+ log_error("Failed to find solution with toggled bit!\n");
+
+ cmp_vars.push_back(y_vec.at(expected_y.width + i));
+ cmp_vals.push_back(true);
+ }
+ else
+ {
+ cmp_vars.push_back(y_vec.at(i));
+ cmp_vals.push_back(y_values.at(i));
+
+ cmp_vars.push_back(y_vec.at(expected_y.width + i));
+ cmp_vals.push_back(false);
+ }
+
+ 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))
+ 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))
+ log_error("Found two distinct solutions to SAT problem.\n");
+ }
log(" SAT model verified.\n");
}