diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-11-25 15:12:01 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-11-25 15:12:01 +0100 |
| commit | bd65e67d8a0ecc71ae0b5df56799e25dd5f2d99a (patch) | |
| tree | 4953de44930847d588092e4b09c8e553946ca71f /passes | |
| parent | 11e811858913cb2d03249d0a7239da10f4af5a7c (diff) | |
| download | yosys-bd65e67d8a0ecc71ae0b5df56799e25dd5f2d99a.tar.gz yosys-bd65e67d8a0ecc71ae0b5df56799e25dd5f2d99a.tar.bz2 yosys-bd65e67d8a0ecc71ae0b5df56799e25dd5f2d99a.zip | |
Improvements in satgen undef handling
Diffstat (limited to 'passes')
| -rw-r--r-- | passes/sat/eval.cc | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index 315e5d7c2..98e235982 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) |