Respect \A_SIGNED for $shift

This reflects the behaviour of $shr/$shl, which sign-extend their A
operands to the size of their output, then do a logical shift (shift in
0-bits).

2 files changed, 19 insertions, 11 deletions

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index e5da6c1e7..5abab8978 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -205,9 +205,8 @@ struct BtorWorker
 			if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor";
 			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)));
+			int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
+			int width = std::max(width_ay, 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;
@@ -224,11 +223,23 @@ struct BtorWorker
 			int sid = get_bv_sid(width);
 			int nid;
 
+			int nid_a;
+			if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) {
+				// sign-extend A up to the width of Y
+				int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed);
+
+				// zero-extend the rest
+				int zeroes = get_sig_nid(Const(0, width-width_ay));
+				nid_a = next_nid++;
+				btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded);
+			} else {
+				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);
+
 			if (btor_op == "shift")
 			{
-				int nid_a = get_sig_nid(cell->getPort(ID::A), width, false);
-				int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
-
 				int nid_r = next_nid++;
 				btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
 
@@ -248,9 +259,6 @@ struct BtorWorker
 			}
 			else
 			{
-				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);
-
 				nid = next_nid++;
 				btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
 			}
diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh
index 3f077201a..0a011932d 100644..100755
--- a/backends/btor/test_cells.sh
+++ b/backends/btor/test_cells.sh
@@ -6,7 +6,7 @@ rm -rf test_cells.tmp
 mkdir -p test_cells.tmp
 cd test_cells.tmp
 
-../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor'
+../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor /$shiftx'
 
 for fn in test_*.il; do
 	../../../yosys -p "
@@ -19,7 +19,7 @@ for fn in test_*.il; do
 		hierarchy -top main
 		write_btor ${fn%.il}.btor
 	"
-	boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
+	btormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
 	if grep " SATISFIABLE" ${fn%.il}.out; then
 		echo "Check failed for ${fn%.il}."
 		exit 1