From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 11 Dec 2017 13:24:19 +0000 (+0100)
Subject: Add btor $shift/$shiftx support
X-Git-Tag: yosys-0.8~246^2~8
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=82d1fd77de31aece7b8a4f31fa53cb9dda2ec5f6;p=yosys.git

Add btor $shift/$shiftx support
---

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index cd6430090..7b80427b8 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -123,7 +123,7 @@ struct BtorWorker
 			if (cell->type.in("$shl", "$sshl")) btor_op = "sll";
 			if (cell->type == "$shr") btor_op = "srl";
 			if (cell->type == "$sshr") btor_op = "sra";
-			// if (cell->type.in("$shift", "$shiftx")) btor_op = "shift";
+			if (cell->type.in("$shift", "$shiftx")) btor_op = "shift";
 			if (cell->type.in("$and", "$_AND_")) btor_op = "and";
 			if (cell->type.in("$or", "$_OR_")) btor_op = "or";
 			if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor";
@@ -139,6 +139,9 @@ struct BtorWorker
 			bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
 			bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
 
+			if (btor_op == "shift" && !b_signed)
+				btor_op = "srl";
+
 			if (cell->type.in("$shl", "$sshl", "$shr", "$sshr"))
 				b_signed = false;
 
@@ -146,11 +149,38 @@ struct BtorWorker
 				btor_op = "srl";
 
 			int sid = get_bv_sid(width);
-			int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
-			int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+			int nid;
 
-			int nid = next_nid++;
-			btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+			if (btor_op == "shift")
+			{
+				int nid_a = get_sig_nid(cell->getPort("\\A"), width, false);
+				int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+
+				int nid_r = next_nid++;
+				btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
+
+				int nid_b_neg = next_nid++;
+				btorf("%d neg %d %d\n", nid_b_neg, sid, nid_b);
+
+				int nid_l = next_nid++;
+				btorf("%d sll %d %d %d\n", nid_l, sid, nid_a, nid_b_neg);
+
+				int sid_bit = get_bv_sid(1);
+				int nid_zero = get_sig_nid(Const(0, width));
+				int nid_b_ltz = next_nid++;
+				btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero);
+
+				nid = next_nid++;
+				btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r);
+			}
+			else
+			{
+				int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
+				int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+
+				nid = next_nid++;
+				btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+			}
 
 			SigSpec sig = sigmap(cell->getPort("\\Y"));
 
diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh
index 0dc8ad854..e0f1a0514 100644
--- 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 /$shift /$shiftx'
+../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod'
 
 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 -v ${fn%.il}.btor > ${fn%.il}.out
+	boolectormc -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