summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-11-25 15:12:01 +0100
committerClifford Wolf <clifford@clifford.at>2013-11-25 15:12:01 +0100
commitbd65e67d8a0ecc71ae0b5df56799e25dd5f2d99a (patch)
tree4953de44930847d588092e4b09c8e553946ca71f /passes
parent11e811858913cb2d03249d0a7239da10f4af5a7c (diff)
Improvements in satgen undef handling
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/eval.cc24
1 files changed, 20 insertions, 4 deletions
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 315e5d7c..98e23598 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -191,11 +191,27 @@ struct VlogHammerReporter
if (expected_bit == RTLIL::State::Sx)
continue;
}
- if (solution_bit != expected_bit)
- log_error("Found error in SAT model: y[%d] = %s, should be %s.\n",
- int(i), log_signal(solution_bit), log_signal(expected_bit));
+ if (solution_bit != expected_bit) {
+ std::string sat_bits, rtl_bits;
+ for (int k = expected_y.width-1; k >= 0; k--) {
+ if (model_undef && y_values.at(expected_y.width+k))
+ sat_bits += "x";
+ else
+ sat_bits += y_values.at(k) ? "1" : "0";
+ rtl_bits += expected_y.chunks.at(k).data.bits.at(0) == RTLIL::State::Sx ? "x" :
+ expected_y.chunks.at(k).data.bits.at(0) == RTLIL::State::S1 ? "1" : "0";
+ }
+ log_error("Found error in SAT model: y[%d] = %s, should be %s:\n SAT: %s\n RTL: %s\n %*s^\n",
+ int(i), log_signal(solution_bit), log_signal(expected_bit),
+ sat_bits.c_str(), rtl_bits.c_str(), expected_y.width-i-1, "");
+ }
}
+ 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");
}
@@ -251,7 +267,7 @@ struct VlogHammerReporter
rtl_sig = sig;
rtl_sig.expand();
sat_check(module, recorded_set_vars, recorded_set_vals, sig, false);
- // sat_check(module, recorded_set_vars, recorded_set_vals, sig, true);
+ sat_check(module, recorded_set_vars, recorded_set_vals, sig, true);
} else if (rtl_sig.width > 0) {
sig.expand();
if (rtl_sig.width != sig.width)