From: Jacob Lifshay <programmerjake@gmail.com>
Date: Tue, 24 May 2022 08:34:25 +0000 (-0700)
Subject: add $divfloor support to write_smt2
X-Git-Tag: divfloor-in-write_smt2-old-test~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d53479a0d6e7c799e29c18cae47f96dfabee9d21;p=yosys.git

add $divfloor support to write_smt2

Fixes: #3330
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a3628197e..ed6f3aff9 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -649,6 +649,27 @@ struct Smt2Worker
 					return export_bvop(cell, "(bvurem A B)", 'd');
 				}
 			}
+			// "div" = flooring division
+			if (cell->type == ID($divfloor)) {
+				if (cell->getParam(ID::A_SIGNED).as_bool()) {
+					// bvsdiv is truncating division, so we can't use it here.
+					int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B)));
+					width = max(width, GetSize(cell->getPort(ID::Y)));
+					auto expr = stringf("(let ("
+							    "(a_neg (bvslt A #b%0*d)) "
+							    "(b_neg (bvslt B #b%0*d))) "
+							    "(let ((abs_a (ite a_neg (bvneg A) A)) "
+							    "(abs_b (ite b_neg (bvneg B) B))) "
+							    "(let ((u (bvudiv abs_a abs_b)) "
+							    "(adj (ite (= #b%0*d (bvurem abs_a abs_b)) #b%0*d #b%0*d))) "
+							    "(ite (= a_neg b_neg) u "
+							    "(bvneg (bvadd u adj))))))",
+							    width, 0, width, 0, width, 0, width, 0, width, 1);
+					return export_bvop(cell, expr, 'd');
+				} else {
+					return export_bvop(cell, "(bvudiv A B)", 'd');
+				}
+			}
 
 			if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) &&
 					2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {