From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 1 Nov 2018 10:40:58 +0000 (+0100)
Subject: Add support for signed $shift/$shiftx in smt2 back-end
X-Git-Tag: yosys-0.9~426
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b6781c6f4ba20ba14d1649a993fc09691921de2b;p=yosys.git

Add support for signed $shift/$shiftx in smt2 back-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e2777ae04..418f8d766 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -554,7 +554,9 @@ struct Smt2Worker
 
 			if (cell->type.in("$shift", "$shiftx")) {
 				if (cell->getParam("\\B_SIGNED").as_bool()) {
-					/* FIXME */
+					return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
+							"(bvlshr A B) (bvlshr A (bvneg B)))",
+							GetSize(cell->getPort("\\B")), 0), 's');
 				} else {
 					return export_bvop(cell, "(bvlshr A B)", 's');
 				}