diff options
| -rw-r--r-- | kernel/calc.cc | 14 | ||||
| -rw-r--r-- | passes/sat/eval.cc | 20 |
2 files changed, 25 insertions, 9 deletions
diff --git a/kernel/calc.cc b/kernel/calc.cc index f4623a65..8034ed2c 100644 --- a/kernel/calc.cc +++ b/kernel/calc.cc @@ -362,15 +362,21 @@ RTLIL::Const RTLIL::const_mul(const RTLIL::Const &arg1, const RTLIL::Const &arg2 RTLIL::Const RTLIL::const_div(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len) { int undef_bit_pos = -1; - BigInteger y = const2big(arg1, signed1, undef_bit_pos) / const2big(arg2, signed2, undef_bit_pos); - return big2const(y, result_len >= 0 ? result_len : std::max(arg1.bits.size(), arg2.bits.size()), std::min(undef_bit_pos, 0)); + BigInteger a = const2big(arg1, signed1, undef_bit_pos); + BigInteger b = const2big(arg2, signed2, undef_bit_pos); + if (b.isZero()) + return RTLIL::Const(RTLIL::State::Sx, result_len); + return big2const(a / b, result_len >= 0 ? result_len : std::max(arg1.bits.size(), arg2.bits.size()), std::min(undef_bit_pos, 0)); } RTLIL::Const RTLIL::const_mod(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len) { int undef_bit_pos = -1; - BigInteger y = const2big(arg1, signed1, undef_bit_pos) % const2big(arg2, signed2, undef_bit_pos); - return big2const(y, result_len >= 0 ? result_len : std::max(arg1.bits.size(), arg2.bits.size()), std::min(undef_bit_pos, 0)); + BigInteger a = const2big(arg1, signed1, undef_bit_pos); + BigInteger b = const2big(arg2, signed2, undef_bit_pos); + if (b.isZero()) + return RTLIL::Const(RTLIL::State::Sx, result_len); + return big2const(a % b, result_len >= 0 ? result_len : std::max(arg1.bits.size(), arg2.bits.size()), std::min(undef_bit_pos, 0)); } RTLIL::Const RTLIL::const_pow(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len) diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index 06428c52..28b9dd6d 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -35,6 +35,7 @@ struct BruteForceEquivChecker RTLIL::SigSpec mod1_inputs, mod1_outputs; RTLIL::SigSpec mod2_inputs, mod2_outputs; int counter, errors; + bool ignore_x_mod1; void run_checker(RTLIL::SigSpec &inputs) { @@ -63,8 +64,16 @@ struct BruteForceEquivChecker log("Failed ConstEval of module 2 outputs at signal %s (input: %s = %s).\n", log_signal(undef2), log_signal(mod1_inputs), log_signal(inputs)); + if (ignore_x_mod1) { + sig1.expand(), sig2.expand(); + for (size_t i = 0; i < sig1.chunks.size(); i++) + if (sig1.chunks.at(i) == RTLIL::SigChunk(RTLIL::State::Sx)) + sig2.chunks.at(i) = RTLIL::SigChunk(RTLIL::State::Sx); + sig1.optimize(), sig2.optimize(); + } + if (sig1 != sig2) { - log("Found counter-example:\n"); + log("Found counter-example (ignore_x_mod1 = %s):\n", ignore_x_mod1 ? "active" : "inactive"); log(" Module 1: %s = %s => %s = %s\n", log_signal(mod1_inputs), log_signal(inputs), log_signal(mod1_outputs), log_signal(sig1)); log(" Module 2: %s = %s => %s = %s\n", log_signal(mod2_inputs), log_signal(inputs), log_signal(mod2_outputs), log_signal(sig2)); errors++; @@ -73,8 +82,8 @@ struct BruteForceEquivChecker counter++; } - BruteForceEquivChecker(RTLIL::Module *mod1, RTLIL::Module *mod2) : - mod1(mod1), mod2(mod2), counter(0), errors(0) + 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()); for (auto &w : mod1->wires) @@ -144,15 +153,16 @@ struct EvalPass : public Pass { shows.push_back(args[++argidx]); continue; } - if (args[argidx] == "-brute_force_equiv_checker" && argidx+2 < args.size()) { + if ((args[argidx] == "-brute_force_equiv_checker" || args[argidx] == "-brute_force_equiv_checker_x") && argidx+2 < args.size()) { /* this should only be used for regression testing of ConstEval -- see tests/xsthammer */ std::string mod1_name = RTLIL::escape_id(args[++argidx]); std::string mod2_name = RTLIL::escape_id(args[++argidx]); + extra_args(args, argidx, design); if (design->modules.count(mod1_name) == 0) log_error("Can't find module `%s'!\n", mod1_name.c_str()); if (design->modules.count(mod2_name) == 0) log_error("Can't find module `%s'!\n", mod2_name.c_str()); - BruteForceEquivChecker checker(design->modules.at(mod1_name), design->modules.at(mod2_name)); + 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("Verified %s = %s (using brute-force check on %d cases).\n", |