diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 86a6c3c72..6ff336a33 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -109,10 +109,12 @@ struct SmvWorker
 		}
 	}
 
-	const char *rvalue(SigSpec sig)
+	const char *rvalue(SigSpec sig, bool skip_sigmap = false, int width = -1, bool is_signed = false)
 	{
+		if (!skip_sigmap)
+			sigmap.apply(sig);
+
 		string s;
-		sigmap.apply(sig);
 		for (auto &c : sig.chunks()) {
 			if (!s.empty())
 				s = " :: " + s;
@@ -129,19 +131,41 @@ struct SmvWorker
 			}
 		}
 
+		if (width >= 0) {
+			if (is_signed) {
+				if (GetSize(sig) > width)
+					s = stringf("signed(resize(%s, %d))", s.c_str(), width);
+				else
+					s = stringf("resize(signed(%s), %d)", s.c_str(), width);
+			} else
+				s = stringf("resize(%s, %d)", s.c_str(), width);
+		} else if (is_signed)
+			s = stringf("signed(%s)", s.c_str());
+
 		strbuf.push_back(s);
 		return strbuf.back().c_str();
 	}
 
-	const char *lvalue(SigSpec sig)
+	const char *rvalue_u(SigSpec sig, int width = -1)
 	{
-		sigmap.apply(sig);
+		return rvalue(sig, false, width, false);
+	}
+
+	const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true)
+	{
+		return rvalue(sig, false, width, is_signed);
+	}
+
+	const char *lvalue(SigSpec sig, bool skip_sigmap = false)
+	{
+		if (!skip_sigmap)
+			sigmap.apply(sig);
 
 		if (sig.is_wire())
-			return rvalue(sig);
+			return rvalue(sig, true);
 
 		const char *temp_id = cid();
-		f << stringf("    %s : unsigned word[%d];\n", temp_id, GetSize(sig));
+		f << stringf("    %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig));
 
 		int offset = 0;
 		for (auto &c : sig.chunks())
@@ -149,7 +173,10 @@ struct SmvWorker
 			log_assert(c.wire != nullptr);
 
 			assign_rhs_chunk rhs;
-			rhs.rhs_expr = stringf("%s[%d:%d]", temp_id, offset+c.width-1, offset);
+			if (offset != 0 || c.width != GetSize(sig))
+				rhs.rhs_expr = stringf("%s[%d:%d]", temp_id, offset+c.width-1, offset);
+			else
+				rhs.rhs_expr = temp_id;
 			rhs.offset = c.offset;
 			rhs.width = c.width;
 
@@ -166,7 +193,30 @@ struct SmvWorker
 		f << stringf("  VAR\n");
 
 		for (auto wire : module->wires())
-			f << stringf("    %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
+		{
+			SigSpec this_sig = wire, driver_sig = sigmap(wire);
+			SigSpec unused_bits_in_this_sig;
+			SigSpec driver_for_unused_bits;
+
+			for (int i = 0; i < GetSize(this_sig); i++)
+				if (this_sig[i] != driver_sig[i]) {
+					unused_bits_in_this_sig.append(this_sig[i]);
+					driver_for_unused_bits.append(driver_sig[i]);
+				}
+
+			if (GetSize(unused_bits_in_this_sig) == GetSize(this_sig))
+			{
+				f << stringf("    -- unused -- %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
+			}
+			else
+			{
+				f << stringf("    %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
+
+				if (!unused_bits_in_this_sig.empty())
+					assignments.push_back(stringf("%s := 0ub%d_0; -- unused %s -- using %s instead", lvalue(unused_bits_in_this_sig, true),
+							GetSize(unused_bits_in_this_sig), log_signal(unused_bits_in_this_sig), log_signal(driver_for_unused_bits)));
+			}
+		}
 
 		for (auto cell : module->cells())
 		{
@@ -212,19 +262,19 @@ struct SmvWorker
 
 				if (cell->getParam("\\A_SIGNED").as_bool())
 				{
-					expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
-					assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")), op.c_str(), expr_a.c_str()));
+					assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
+							op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
 				}
 				else
 				{
-					expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
-					assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), expr_a.c_str()));
+					assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
+							op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
 				}
 
 				continue;
 			}
 
-			if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$and", "$or", "$xor", "$xnor"))
+			if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
 			{
 				int width = GetSize(cell->getPort("\\Y"));
 				string expr_a, expr_b, op;
@@ -232,8 +282,6 @@ struct SmvWorker
 				if (cell->type == "$add")  op = "+";
 				if (cell->type == "$sub")  op = "-";
 				if (cell->type == "$mul")  op = "*";
-				if (cell->type == "$div")  op = "/";
-				if (cell->type == "$mod")  op = "%";
 				if (cell->type == "$and")  op = "&";
 				if (cell->type == "$or")   op = "|";
 				if (cell->type == "$xor")  op = "xor";
@@ -241,15 +289,37 @@ struct SmvWorker
 
 				if (cell->getParam("\\A_SIGNED").as_bool())
 				{
-					expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
-					expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
-					assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")), expr_a.c_str(), op.c_str(), expr_b.c_str()));
+					assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
+							rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
 				}
 				else
 				{
-					expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
-					expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
-					assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")), expr_a.c_str(), op.c_str(), expr_b.c_str()));
+					assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
+							rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
+				}
+
+				continue;
+			}
+
+			if (cell->type.in("$div", "$mod"))
+			{
+				int width_y = GetSize(cell->getPort("\\Y"));
+				int width = std::max(width_y, GetSize(cell->getPort("\\A")));
+				width = std::max(width, GetSize(cell->getPort("\\B")));
+				string expr_a, expr_b, op;
+
+				if (cell->type == "$div")  op = "/";
+				if (cell->type == "$mod")  op = "mod";
+
+				if (cell->getParam("\\A_SIGNED").as_bool())
+				{
+					assignments.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
+							rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
+				}
+				else
+				{
+					assignments.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
+							rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
 				}
 
 				continue;
@@ -294,7 +364,7 @@ struct SmvWorker
 				const char *expr_y = lvalue(cell->getPort("\\Y"));
 				string expr;
 
-				if (cell->type == "$reduce_and")  expr = stringf("%s == !0ub%d_0", expr_a, width_a);
+				if (cell->type == "$reduce_and")  expr = stringf("%s = !0ub%d_0", expr_a, width_a);
 				if (cell->type == "$reduce_or")   expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 				if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 
@@ -344,7 +414,7 @@ struct SmvWorker
 				int width_a = GetSize(cell->getPort("\\A"));
 				int width_y = GetSize(cell->getPort("\\Y"));
 
-				string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
+				string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
 				const char *expr_y = lvalue(cell->getPort("\\Y"));
 
 				assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
@@ -401,7 +471,7 @@ struct SmvWorker
 
 			if (cell->type == "$_MUX_")
 			{
-				assignments.push_back(stringf("%s := %s ? %s : %s;", lvalue(cell->getPort("\\Y")),
+				assignments.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
 						rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
 				continue;
 			}
diff --git a/tests/smv/.gitignore b/tests/smv/.gitignore
new file mode 100644
index 000000000..9c595a6fb
--- /dev/null
+++ b/tests/smv/.gitignore
@@ -0,0 +1 @@
+temp
diff --git a/tests/smv/run-single.sh b/tests/smv/run-single.sh
new file mode 100644
index 000000000..a261f4ea6
--- /dev/null
+++ b/tests/smv/run-single.sh
@@ -0,0 +1,33 @@
+#!/bin/bash
+
+cat > $1.tpl <<EOT
+%module main
+  INVARSPEC ! bool(_trigger)
+EOT
+
+cat > $1.ys <<EOT
+echo on
+
+read_ilang $1.il
+hierarchy; proc; opt
+rename -top uut
+design -save gold
+
+synth
+design -stash gate
+
+design -copy-from gold -as gold uut
+design -copy-from gate -as gate uut
+miter -equiv -flatten gold gate main
+hierarchy -top main
+
+dump
+write_smv -tpl $1.tpl $1.smv
+EOT
+
+set -ex
+
+../../yosys -l $1.log -q $1.ys
+NuSMV -bmc $1.smv >> $1.log
+grep "^-- invariant .* is true" $1.log
+
diff --git a/tests/smv/run-test.sh b/tests/smv/run-test.sh
new file mode 100755
index 000000000..c61f67d30
--- /dev/null
+++ b/tests/smv/run-test.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+set -ex
+
+rm -rf temp
+mkdir -p temp
+
+../../yosys -p 'test_cell -muxdiv -w temp/test all'
+rm -f temp/test_{alu,fa,lcu,lut,macc}_*
+
+cat > temp/makefile << "EOT"
+all: $(addsuffix .ok,$(basename $(wildcard temp/test_*.il)))
+%.ok: %.il
+	bash run-single.sh $(basename $<)
+	touch $@
+EOT
+
+${MAKE:-make} -f temp/makefile
+