Merge pull request #1885 from Xiretza/mod-rem-cells

Fix modulo/remainder semantics

6 files changed, 98 insertions, 11 deletions

diff --git a/kernel/calc.cc b/kernel/calc.cc
index 4a4840771..ae18809d3 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -489,6 +489,7 @@ RTLIL::Const RTLIL::const_mul(const RTLIL::Const &arg1, const RTLIL::Const &arg2
 	return big2const(y, result_len >= 0 ? result_len : max(arg1.bits.size(), arg2.bits.size()), min(undef_bit_pos, 0));
 }
 
+// truncating division
 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;
@@ -502,6 +503,7 @@ RTLIL::Const RTLIL::const_div(const RTLIL::Const &arg1, const RTLIL::Const &arg2
 	return big2const(result_neg ? -(a / b) : (a / b), result_len >= 0 ? result_len : max(arg1.bits.size(), arg2.bits.size()), min(undef_bit_pos, 0));
 }
 
+// truncating modulo
 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;
@@ -515,6 +517,51 @@ RTLIL::Const RTLIL::const_mod(const RTLIL::Const &arg1, const RTLIL::Const &arg2
 	return big2const(result_neg ? -(a % b) : (a % b), result_len >= 0 ? result_len : max(arg1.bits.size(), arg2.bits.size()), min(undef_bit_pos, 0));
 }
 
+RTLIL::Const RTLIL::const_divfloor(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+	int undef_bit_pos = -1;
+	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);
+
+	bool result_pos = (a.getSign() == BigInteger::negative) == (b.getSign() == BigInteger::negative);
+	a = a.getSign() == BigInteger::negative ? -a : a;
+	b = b.getSign() == BigInteger::negative ? -b : b;
+	BigInteger result;
+
+	if (result_pos || a == 0) {
+		result = a / b;
+	} else {
+		// bigint division with negative numbers is wonky, make sure we only negate at the very end
+		result = -((a + b - 1) / b);
+	}
+	return big2const(result, result_len >= 0 ? result_len : max(arg1.bits.size(), arg2.bits.size()), min(undef_bit_pos, 0));
+}
+
+RTLIL::Const RTLIL::const_modfloor(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+	int undef_bit_pos = -1;
+	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);
+
+	BigInteger::Sign a_sign = a.getSign();
+	BigInteger::Sign b_sign = b.getSign();
+	a = a_sign == BigInteger::negative ? -a : a;
+	b = b_sign == BigInteger::negative ? -b : b;
+	BigInteger truncated = a_sign == BigInteger::negative ? -(a % b) : (a % b);
+	BigInteger modulo;
+
+	if (truncated == 0 || (a_sign == b_sign)) {
+		modulo = truncated;
+	} else {
+		modulo = b_sign == BigInteger::negative ? truncated - b : truncated + b;
+	}
+	return big2const(modulo, result_len >= 0 ? result_len : max(arg1.bits.size(), arg2.bits.size()), 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)
 {
 	int undef_bit_pos = -1;
diff --git a/kernel/celledges.cc b/kernel/celledges.cc
index 54e0168e2..314e7c77e 100644
--- a/kernel/celledges.cc
+++ b/kernel/celledges.cc
@@ -187,7 +187,7 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
 		return true;
 	}
 
-	// FIXME: $mul $div $mod $slice $concat
+	// FIXME: $mul $div $mod $divfloor $modfloor $slice $concat
 	// FIXME: $lut $sop $alu $lcu $macc $fa
 
 	return false;
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 450865ce9..db54436cb 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -114,7 +114,7 @@ struct CellTypes
 			ID($and), ID($or), ID($xor), ID($xnor),
 			ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx),
 			ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt),
-			ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($pow),
+			ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow),
 			ID($logic_and), ID($logic_or), ID($concat), ID($macc)
 		};
 
@@ -304,6 +304,8 @@ struct CellTypes
 		HANDLE_CELL_TYPE(mul)
 		HANDLE_CELL_TYPE(div)
 		HANDLE_CELL_TYPE(mod)
+		HANDLE_CELL_TYPE(divfloor)
+		HANDLE_CELL_TYPE(modfloor)
 		HANDLE_CELL_TYPE(pow)
 		HANDLE_CELL_TYPE(pos)
 		HANDLE_CELL_TYPE(neg)
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 196e301b6..ca4201b53 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -948,7 +948,7 @@ namespace {
 				return;
 			}
 
-			if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($pow))) {
+			if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow))) {
 				param_bool(ID::A_SIGNED);
 				param_bool(ID::B_SIGNED);
 				port(ID::A, param(ID::A_WIDTH));
@@ -1949,6 +1949,8 @@ DEF_METHOD(Sub,      max(sig_a.size(), sig_b.size()), ID($sub))
 DEF_METHOD(Mul,      max(sig_a.size(), sig_b.size()), ID($mul))
 DEF_METHOD(Div,      max(sig_a.size(), sig_b.size()), ID($div))
 DEF_METHOD(Mod,      max(sig_a.size(), sig_b.size()), ID($mod))
+DEF_METHOD(DivFloor, max(sig_a.size(), sig_b.size()), ID($divfloor))
+DEF_METHOD(ModFloor, max(sig_a.size(), sig_b.size()), ID($modfloor))
 DEF_METHOD(LogicAnd, 1, ID($logic_and))
 DEF_METHOD(LogicOr,  1, ID($logic_or))
 #undef DEF_METHOD
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 91d6a9f77..8228523d5 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -468,6 +468,8 @@ namespace RTLIL
 	RTLIL::Const const_sub         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_mul         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_div         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+	RTLIL::Const const_divfloor    (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+	RTLIL::Const const_modfloor    (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_mod         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 	RTLIL::Const const_pow         (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
 
@@ -1204,8 +1206,12 @@ public:
 	RTLIL::Cell* addAdd (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
 	RTLIL::Cell* addSub (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
 	RTLIL::Cell* addMul (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
+	// truncating division
 	RTLIL::Cell* addDiv (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
+	// truncating modulo
 	RTLIL::Cell* addMod (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
+	RTLIL::Cell* addDivFloor (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
+	RTLIL::Cell* addModFloor (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
 	RTLIL::Cell* addPow (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, bool a_signed = false, bool b_signed = false, const std::string &src = "");
 
 	RTLIL::Cell* addLogicNot (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
@@ -1303,8 +1309,12 @@ public:
 	RTLIL::SigSpec Add (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool is_signed = false, const std::string &src = "");
 	RTLIL::SigSpec Sub (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool is_signed = false, const std::string &src = "");
 	RTLIL::SigSpec Mul (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool is_signed = false, const std::string &src = "");
+	// truncating division
 	RTLIL::SigSpec Div (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool is_signed = false, const std::string &src = "");
+	// truncating modulo
 	RTLIL::SigSpec Mod (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool is_signed = false, const std::string &src = "");
+	RTLIL::SigSpec DivFloor (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool is_signed = false, const std::string &src = "");
+	RTLIL::SigSpec ModFloor (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool is_signed = false, const std::string &src = "");
 	RTLIL::SigSpec Pow (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, bool a_signed = false, bool b_signed = false, const std::string &src = "");
 
 	RTLIL::SigSpec LogicNot (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, bool is_signed = false, const std::string &src = "");
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 88b84b7e6..3929a8708 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -279,7 +279,7 @@ struct SatGen
 		bool arith_undef_handled = false;
 		bool is_arith_compare = cell->type.in(ID($lt), ID($le), ID($ge), ID($gt));
 
-		if (model_undef && (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod)) || is_arith_compare))
+		if (model_undef && (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)) || is_arith_compare))
 		{
 			std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
 			std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
@@ -293,7 +293,7 @@ struct SatGen
 			int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
 			int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
 
-			if (cell->type.in(ID($div), ID($mod))) {
+			if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
 				std::vector<int> b = importSigSpec(cell->getPort(ID::B), timestep);
 				undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
 			}
@@ -935,7 +935,7 @@ struct SatGen
 			return true;
 		}
 
-		if (cell->type.in(ID($div), ID($mod)))
+		if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor)))
 		{
 			std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
 			std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
@@ -970,23 +970,48 @@ struct SatGen
 			}
 
 			std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
+
+			// modulo calculation
+			std::vector<int> modulo_trunc;
+			int floored_eq_trunc;
+			if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
+				modulo_trunc = ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf);
+				// floor == trunc when sgn(a) == sgn(b) or trunc == 0
+				floored_eq_trunc = ez->OR(ez->IFF(a.back(), b.back()), ez->NOT(ez->expression(ezSAT::OpOr, modulo_trunc)));
+			} else {
+				modulo_trunc = chain_buf;
+				floored_eq_trunc = ez->CONST_TRUE;
+			}
+
 			if (cell->type == ID($div)) {
 				if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
 					ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
 				else
 					ez->assume(ez->vec_eq(y_tmp, y_u));
-			} else {
+			} else if (cell->type == ID($mod)) {
+				ez->assume(ez->vec_eq(y_tmp, modulo_trunc));
+			} else if (cell->type == ID($divfloor)) {
 				if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
-					ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf)));
+					ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(
+						ez->XOR(a.back(), b.back()),
+						ez->vec_neg(ez->vec_ite(
+							ez->vec_reduce_or(modulo_trunc),
+							ez->vec_add(y_u, ez->vec_const_unsigned(1, y_u.size())),
+							y_u
+						)),
+						y_u
+					)));
 				else
-					ez->assume(ez->vec_eq(y_tmp, chain_buf));
+					ez->assume(ez->vec_eq(y_tmp, y_u));
+			} else if (cell->type == ID($modfloor)) {
+				ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(floored_eq_trunc, modulo_trunc, ez->vec_add(modulo_trunc, b))));
 			}
 
 			if (ignore_div_by_zero) {
 				ez->assume(ez->expression(ezSAT::OpOr, b));
 			} else {
 				std::vector<int> div_zero_result;
-				if (cell->type == ID($div)) {
+				if (cell->type.in(ID($div), ID($divfloor))) {
 					if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
 						std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
 						std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
@@ -996,7 +1021,8 @@ struct SatGen
 						div_zero_result.insert(div_zero_result.end(), cell->getPort(ID::A).size(), ez->CONST_TRUE);
 						div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
 					}
-				} else {
+				} else if (cell->type.in(ID($mod), ID($modfloor))) {
+					// a mod 0 = a
 					int copy_a_bits = min(cell->getPort(ID::A).size(), cell->getPort(ID::B).size());
 					div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
 					if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())