Add flooring modulo operator

The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $modfloor cell provides this flooring modulo (also known as "remainder"
in several languages, but this name is ambiguous).

This commit also fixes the handling of $mod in opt_expr, which was
previously optimized as if it was $modfloor.

1 files changed, 10 insertions, 4 deletions

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 14c8484e8..2816d3246 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -266,20 +266,26 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in(ID($div), ID($mod)))
+		if (cell->type.in(ID($div), ID($mod), ID($modfloor)))
 		{
+			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
+			bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
+
 			string btor_op;
 			if (cell->type == ID($div)) btor_op = "div";
+			// "rem" = truncating modulo
 			if (cell->type == ID($mod)) btor_op = "rem";
+			// "mod" = flooring modulo
+			if (cell->type == ID($modfloor)) {
+				// "umod" doesn't exist because it's the same as "urem"
+				btor_op = a_signed || b_signed ? "mod" : "rem";
+			}
 			log_assert(!btor_op.empty());
 
 			int width = GetSize(cell->getPort(ID::Y));
 			width = std::max(width, GetSize(cell->getPort(ID::A)));
 			width = std::max(width, GetSize(cell->getPort(ID::B)));
 
-			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
-			bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
-
 			int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
 			int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);