From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 15 Aug 2013 09:09:30 +0000 (+0200)
Subject: Added eval -brute_force_equiv_checker_x mode
X-Git-Tag: yosys-0.2.0~504
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0e93e04d1cc196264b0bbcf1aafcfba0adb2ea0;p=yosys.git

Added eval -brute_force_equiv_checker_x mode
---

diff --git a/kernel/calc.cc b/kernel/calc.cc
index f4623a65b..8034ed2ce 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 06428c525..28b9dd6dd 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",