Progress in SMV back-end

diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 86a6c3c72322c44e82d474970fec17a5fa9af151..6ff336a33853374b746bce6883c7db92ef1c0c17 100644 (file)
--- 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 (file)
index 0000000..9c595a6
--- /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 (file)
index 0000000..a261f4e
--- /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 (executable)
index 0000000..c61f67d
--- /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
+