From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 9 Mar 2019 21:19:41 +0000 (-0800)
Subject: Fix signed $shift/$shiftx handling in write_smt2
X-Git-Tag: yosys-0.9~251
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94f995ee3784e1a94a484fd399be2be4793d4e41;p=yosys.git

Fix signed $shift/$shiftx handling in write_smt2

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

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a26bff57b..688535f33 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -416,6 +416,7 @@ struct Smt2Worker
 		for (char ch : expr) {
 			if (ch == 'A') processed_expr += get_bv(sig_a);
 			else if (ch == 'B') processed_expr += get_bv(sig_b);
+			else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
 			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
 			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
 			else processed_expr += ch;
@@ -554,7 +555,7 @@ struct Smt2Worker
 
 			if (cell->type.in("$shift", "$shiftx")) {
 				if (cell->getParam("\\B_SIGNED").as_bool()) {
-					return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
+					return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
 							"(bvlshr A B) (bvlshr A (bvneg B)))",
 							GetSize(cell->getPort("\\B")), 0), 's');
 				} else {