cxxrtl: make alias analysis outlining-aware.
[yosys.git] / backends / smv / smv.cc
index 1758995d12228aea9e78e21e2157f5f342af56d8..4e5c6050db61be169b5d7c9105fc7412dd2195e6 100644 (file)
@@ -2,11 +2,11 @@
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  
+ *
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
  *  copyright notice and this permission notice appear in all copies.
- *  
+ *
  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -40,14 +40,9 @@ struct SmvWorker
        pool<shared_str> used_names;
        vector<shared_str> strbuf;
 
-       struct assign_rhs_chunk {
-               string rhs_expr;
-               int offset, width;
-               bool operator<(const assign_rhs_chunk &other) const { return offset < other.offset; }
-       };
-
-       dict<Wire*, vector<assign_rhs_chunk>> partial_assignments;
-       vector<string> assignments;
+       pool<Wire*> partial_assignment_wires;
+       dict<SigBit, std::pair<const char*, int>> partial_assignment_bits;
+       vector<string> inputvars, vars, definitions, assignments, invarspecs;
 
        const char *cid()
        {
@@ -66,7 +61,7 @@ struct SmvWorker
                {
                        string name = stringf("_%s", id.c_str());
 
-                       if (name.substr(0, 2) == "_\\")
+                       if (name.compare(0, 2, "_\\") == 0)
                                name = "_" + name.substr(2);
 
                        for (auto &c : name) {
@@ -109,11 +104,46 @@ struct SmvWorker
                }
        }
 
-       const char *rvalue(SigSpec sig)
+       const char *rvalue(SigSpec sig, int width = -1, bool is_signed = false)
        {
                string s;
+               int count_chunks = 0;
                sigmap.apply(sig);
+
+               for (int i = 0; i < GetSize(sig); i++)
+                       if (partial_assignment_bits.count(sig[i]))
+                       {
+                               int width = 1;
+                               const auto &bit_a = partial_assignment_bits.at(sig[i]);
+
+                               while (i+width < GetSize(sig))
+                               {
+                                       if (!partial_assignment_bits.count(sig[i+width]))
+                                               break;
+
+                                       const auto &bit_b = partial_assignment_bits.at(sig[i+width]);
+                                       if (strcmp(bit_a.first, bit_b.first))
+                                               break;
+                                       if (bit_a.second+width != bit_b.second)
+                                               break;
+
+                                       width++;
+                               }
+
+                               if (i+width < GetSize(sig))
+                                       s = stringf("%s :: ", rvalue(sig.extract(i+width, GetSize(sig)-(width+i))));
+
+                               s += stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second);
+
+                               if (i > 0)
+                                       s += stringf(" :: %s", rvalue(sig.extract(0, i)));
+
+                               count_chunks = 3;
+                               goto continue_with_resize;
+                       }
+
                for (auto &c : sig.chunks()) {
+                       count_chunks++;
                        if (!s.empty())
                                s = " :: " + s;
                        if (c.wire) {
@@ -129,10 +159,34 @@ struct SmvWorker
                        }
                }
 
+       continue_with_resize:;
+               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());
+               else if (count_chunks > 1)
+                       s = stringf("(%s)", s.c_str());
+
                strbuf.push_back(s);
                return strbuf.back().c_str();
        }
 
+       const char *rvalue_u(SigSpec sig, int width = -1)
+       {
+               return rvalue(sig, width, false);
+       }
+
+       const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true)
+       {
+               return rvalue(sig, width, is_signed);
+       }
+
        const char *lvalue(SigSpec sig)
        {
                sigmap.apply(sig);
@@ -141,20 +195,13 @@ struct SmvWorker
                        return rvalue(sig);
 
                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())
-               {
-                       log_assert(c.wire != nullptr);
-
-                       assign_rhs_chunk rhs;
-                       rhs.rhs_expr = stringf("%s[%d:%d]", temp_id, offset+c.width-1, offset);
-                       rhs.offset = c.offset;
-                       rhs.width = c.width;
-
-                       partial_assignments[c.wire].push_back(rhs);
-                       offset += c.width;
+               for (auto bit : sig) {
+                       log_assert(bit.wire != nullptr);
+                       partial_assignment_wires.insert(bit.wire);
+                       partial_assignment_bits[bit] = std::pair<const char*, int>(temp_id, offset++);
                }
 
                return temp_id;
@@ -163,260 +210,499 @@ struct SmvWorker
        void run()
        {
                f << stringf("MODULE %s\n", cid(module->name));
-               f << stringf("  VAR\n");
 
                for (auto wire : module->wires())
-                       f << stringf("    %s : unsigned word[%d];\n", cid(wire->name), wire->width);
+               {
+                       if (SigSpec(wire) != sigmap(wire))
+                               partial_assignment_wires.insert(wire);
+
+                       if (wire->port_input)
+                               inputvars.push_back(stringf("%s : unsigned word[%d]; -- %s", cid(wire->name), wire->width, log_id(wire)));
+
+                       if (wire->attributes.count(ID::init))
+                               assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at(ID::init))));
+               }
 
                for (auto cell : module->cells())
                {
                        // FIXME: $slice, $concat, $mem
 
-                       if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
+                       if (cell->type.in(ID($assert)))
                        {
-                               int width_y = GetSize(cell->getPort("\\Y"));
-                               int width = std::max(GetSize(cell->getPort("\\A")), width_y);
-                               bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
-                               string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
+                               SigSpec sig_a = cell->getPort(ID::A);
+                               SigSpec sig_en = cell->getPort(ID::EN);
+
+                               invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a)));
+
+                               continue;
+                       }
+
+                       if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
+                       {
+                               SigSpec sig_a = cell->getPort(ID::A);
+                               SigSpec sig_b = cell->getPort(ID::B);
+
+                               int width_y = GetSize(cell->getPort(ID::Y));
+                               int shift_b_width = GetSize(sig_b);
+                               int width_ay = max(GetSize(sig_a), width_y);
+                               int width = width_ay;
+
+                               for (int i = 1, j = 0;; i <<= 1, j++)
+                                       if (width_ay < i) {
+                                               width = i-1;
+                                               shift_b_width = min(shift_b_width, j);
+                                               break;
+                                       }
+
+                               bool signed_a = cell->getParam(ID::A_SIGNED).as_bool();
+                               bool signed_b = cell->getParam(ID::B_SIGNED).as_bool();
+                               string op = cell->type.in(ID($shl), ID($sshl)) ? "<<" : ">>";
                                string expr, expr_a;
 
-                               if (signed_a) {
-                                       expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
-                               } else
-                                       expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
-
-                               if (cell->type == "$sshr" && signed_a) {
-                                       expr = stringf("resize(%s %s %s, %d)", expr_a.c_str(), op.c_str(), rvalue(cell->getPort("\\B")), width_y);
-                               } else {
-                                       if (signed_a)
-                                               expr_a = "unsigned(" + expr_a + ")";
-                                       if (cell->type.in("$shift", "$shiftx") && cell->getParam("\\B_SIGNED").as_bool())
-                                               expr = stringf("resize(%s %s signed(%s), %d)", expr_a.c_str(), op.c_str(), rvalue(cell->getPort("\\B")), width_y);
+                               if (cell->type == ID($sshr) && signed_a)
+                               {
+                                       expr_a = rvalue_s(sig_a, width);
+                                       expr = stringf("resize(unsigned(%s %s %s), %d)", expr_a.c_str(), op.c_str(), rvalue(sig_b.extract(0, shift_b_width)), width_y);
+                                       if (shift_b_width < GetSize(sig_b))
+                                               expr = stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s",
+                                                               rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
+                                                               rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
+                               }
+                               else if (cell->type.in(ID($shift), ID($shiftx)) && signed_b)
+                               {
+                                       expr_a = rvalue_u(sig_a, width);
+
+                                       const char *b_shr = rvalue_u(sig_b);
+                                       const char *b_shl = cid();
+
+//                                     f << stringf("    %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b));
+                                       definitions.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b)));
+
+                                       string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y);
+                                       string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y);
+
+                                       if (shift_b_width < GetSize(sig_b)) {
+                                               expr_shl = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl, GetSize(sig_b)-1, shift_b_width,
+                                                               GetSize(sig_b)-shift_b_width, width_y, expr_shl.c_str());
+                                               expr_shr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr, GetSize(sig_b)-1, shift_b_width,
+                                                               GetSize(sig_b)-shift_b_width, width_y, expr_shr.c_str());
+                                       }
+
+                                       expr = stringf("bool(%s) ? %s : %s", rvalue(sig_b[GetSize(sig_b)-1]), expr_shl.c_str(), expr_shr.c_str());
+                               }
+                               else
+                               {
+                                       if (cell->type.in(ID($shift), ID($shiftx)) || !signed_a)
+                                               expr_a = rvalue_u(sig_a, width);
                                        else
-                                               expr = stringf("resize(%s %s %s, %d)", expr_a.c_str(), op.c_str(), rvalue(cell->getPort("\\B")), width_y);
+                                               expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
+
+                                       expr = stringf("resize(%s %s %s[%d:0], %d)", expr_a.c_str(), op.c_str(), rvalue_u(sig_b), shift_b_width-1, width_y);
+                                       if (shift_b_width < GetSize(sig_b))
+                                               expr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b), GetSize(sig_b)-1, shift_b_width,
+                                                               GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
                                }
 
-                               assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
+                               definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
 
                                continue;
                        }
 
-                       if (cell->type.in("$not", "$pos", "$neg"))
+                       if (cell->type.in(ID($not), ID($pos), ID($neg)))
                        {
-                               int width = GetSize(cell->getPort("\\Y"));
+                               int width = GetSize(cell->getPort(ID::Y));
                                string expr_a, op;
 
-                               if (cell->type == "$not")  op = "!";
-                               if (cell->type == "$pos")  op = "";
-                               if (cell->type == "$neg")  op = "-";
+                               if (cell->type == ID($not))  op = "!";
+                               if (cell->type == ID($pos))  op = "";
+                               if (cell->type == ID($neg))  op = "-";
+
+                               if (cell->getParam(ID::A_SIGNED).as_bool())
+                               {
+                                       definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort(ID::Y)),
+                                                       op.c_str(), rvalue_s(cell->getPort(ID::A), width)));
+                               }
+                               else
+                               {
+                                       definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)),
+                                                       op.c_str(), rvalue_u(cell->getPort(ID::A), width)));
+                               }
+
+                               continue;
+                       }
+
+                       if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor)))
+                       {
+                               int width = GetSize(cell->getPort(ID::Y));
+                               string expr_a, expr_b, op;
+
+                               if (cell->type == ID($add))  op = "+";
+                               if (cell->type == ID($sub))  op = "-";
+                               if (cell->type == ID($mul))  op = "*";
+                               if (cell->type == ID($and))  op = "&";
+                               if (cell->type == ID($or))   op = "|";
+                               if (cell->type == ID($xor))  op = "xor";
+                               if (cell->type == ID($xnor)) op = "xnor";
 
-                               if (cell->getParam("\\A_SIGNED").as_bool())
+                               if (cell->getParam(ID::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()));
+                                       definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort(ID::Y)),
+                                                       rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), 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()));
+                                       definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
+                                                       rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width)));
                                }
 
                                continue;
                        }
 
-                       if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$and", "$or", "$xor", "$xnor"))
+                       // SMV has a "mod" operator, but its semantics don't seem to be well-defined - to be safe, don't generate it at all
+                       if (cell->type.in(ID($div)/*, ID($mod), ID($modfloor)*/))
                        {
-                               int width = GetSize(cell->getPort("\\Y"));
+                               int width_y = GetSize(cell->getPort(ID::Y));
+                               int width = max(width_y, GetSize(cell->getPort(ID::A)));
+                               width = max(width, GetSize(cell->getPort(ID::B)));
                                string expr_a, expr_b, op;
 
-                               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";
-                               if (cell->type == "$xnor") op = "xnor";
-
-                               if (cell->getParam("\\A_SIGNED").as_bool())
+                               if (cell->type == ID($div))  op = "/";
+                               //if (cell->type == ID($mod))  op = "mod";
+
+                               if (cell->getParam(ID::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()));
+                                       definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
+                                                       rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width), width_y));
                                }
                                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()));
+                                       definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort(ID::Y)),
+                                                       rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width), width_y));
                                }
 
                                continue;
                        }
 
-                       if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
+                       if (cell->type.in(ID($eq), ID($ne), ID($eqx), ID($nex), ID($lt), ID($le), ID($ge), ID($gt)))
                        {
-                               int width = std::max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
+                               int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B)));
                                string expr_a, expr_b, op;
 
-                               if (cell->type == "$eq")  op = "=";
-                               if (cell->type == "$ne")  op = "!=";
-                               if (cell->type == "$eqx") op = "=";
-                               if (cell->type == "$nex") op = "!=";
-                               if (cell->type == "$lt")  op = "<";
-                               if (cell->type == "$le")  op = "<=";
-                               if (cell->type == "$ge")  op = ">=";
-                               if (cell->type == "$gt")  op = ">";
+                               if (cell->type == ID($eq))  op = "=";
+                               if (cell->type == ID($ne))  op = "!=";
+                               if (cell->type == ID($eqx)) op = "=";
+                               if (cell->type == ID($nex)) op = "!=";
+                               if (cell->type == ID($lt))  op = "<";
+                               if (cell->type == ID($le))  op = "<=";
+                               if (cell->type == ID($ge))  op = ">=";
+                               if (cell->type == ID($gt))  op = ">";
 
-                               if (cell->getParam("\\A_SIGNED").as_bool())
+                               if (cell->getParam(ID::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);
+                                       expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::A)), width);
+                                       expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::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);
+                                       expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::A)), width);
+                                       expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::B)), width);
                                }
 
-                               assignments.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
-                                               expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
+                               definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
+                                               expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort(ID::Y))));
 
                                continue;
                        }
 
-                       if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
+                       if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)))
                        {
-                               int width_a = GetSize(cell->getPort("\\A"));
-                               int width_y = GetSize(cell->getPort("\\Y"));
-                               const char *expr_a = rvalue(cell->getPort("\\A"));
-                               const char *expr_y = lvalue(cell->getPort("\\Y"));
+                               int width_a = GetSize(cell->getPort(ID::A));
+                               int width_y = GetSize(cell->getPort(ID::Y));
+                               const char *expr_a = rvalue(cell->getPort(ID::A));
+                               const char *expr_y = lvalue(cell->getPort(ID::Y));
                                string expr;
 
-                               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);
+                               if (cell->type == ID($reduce_and))  expr = stringf("%s = !0ub%d_0", expr_a, width_a);
+                               if (cell->type == ID($reduce_or))   expr = stringf("%s != 0ub%d_0", expr_a, width_a);
+                               if (cell->type == ID($reduce_bool)) expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 
-                               assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
+                               definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
                                continue;
                        }
 
-                       if (cell->type.in("$reduce_xor", "$reduce_xnor"))
+                       if (cell->type.in(ID($reduce_xor), ID($reduce_xnor)))
                        {
-                               int width_y = GetSize(cell->getPort("\\Y"));
-                               const char *expr_y = lvalue(cell->getPort("\\Y"));
+                               int width_y = GetSize(cell->getPort(ID::Y));
+                               const char *expr_y = lvalue(cell->getPort(ID::Y));
                                string expr;
 
-                               for (auto bit : cell->getPort("\\A")) {
+                               for (auto bit : cell->getPort(ID::A)) {
                                        if (!expr.empty())
                                                expr += " xor ";
                                        expr += rvalue(bit);
                                }
 
-                               if (cell->type == "$reduce_xnor")
+                               if (cell->type == ID($reduce_xnor))
                                        expr = "!(" + expr + ")";
 
-                               assignments.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
+                               definitions.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
                                continue;
                        }
 
-                       if (cell->type.in("$logic_and", "$logic_or"))
+                       if (cell->type.in(ID($logic_and), ID($logic_or)))
                        {
-                               int width_a = GetSize(cell->getPort("\\A"));
-                               int width_b = GetSize(cell->getPort("\\B"));
-                               int width_y = GetSize(cell->getPort("\\Y"));
+                               int width_a = GetSize(cell->getPort(ID::A));
+                               int width_b = GetSize(cell->getPort(ID::B));
+                               int width_y = GetSize(cell->getPort(ID::Y));
 
-                               string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
-                               string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
-                               const char *expr_y = lvalue(cell->getPort("\\Y"));
+                               string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
+                               string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::B)), width_b);
+                               const char *expr_y = lvalue(cell->getPort(ID::Y));
 
                                string expr;
-                               if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
-                               if (cell->type == "$logic_or")  expr = expr_a + " | " + expr_b;
+                               if (cell->type == ID($logic_and)) expr = expr_a + " & " + expr_b;
+                               if (cell->type == ID($logic_or))  expr = expr_a + " | " + expr_b;
 
-                               assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
+                               definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
                                continue;
                        }
 
-                       if (cell->type.in("$logic_not"))
+                       if (cell->type.in(ID($logic_not)))
                        {
-                               int width_a = GetSize(cell->getPort("\\A"));
-                               int width_y = GetSize(cell->getPort("\\Y"));
+                               int width_a = GetSize(cell->getPort(ID::A));
+                               int width_y = GetSize(cell->getPort(ID::Y));
 
-                               string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
-                               const char *expr_y = lvalue(cell->getPort("\\Y"));
+                               string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
+                               const char *expr_y = lvalue(cell->getPort(ID::Y));
 
-                               assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
+                               definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
                                continue;
                        }
 
-                       if (cell->type.in("$mux", "$pmux"))
+                       if (cell->type.in(ID($mux), ID($pmux)))
                        {
-                               int width = GetSize(cell->getPort("\\Y"));
-                               SigSpec sig_a = cell->getPort("\\A");
-                               SigSpec sig_b = cell->getPort("\\B");
-                               SigSpec sig_s = cell->getPort("\\S");
+                               int width = GetSize(cell->getPort(ID::Y));
+                               SigSpec sig_a = cell->getPort(ID::A);
+                               SigSpec sig_b = cell->getPort(ID::B);
+                               SigSpec sig_s = cell->getPort(ID::S);
 
                                string expr;
                                for (int i = 0; i < GetSize(sig_s); i++)
                                        expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
                                expr += rvalue(sig_a);
 
-                               assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
+                               definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
+                               continue;
+                       }
+
+                       if (cell->type == ID($dff))
+                       {
+                               vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort(ID::Q)), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))));
+                               assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort(ID::Q)), rvalue(cell->getPort(ID::D))));
                                continue;
                        }
 
-                       if (cell->type == "$dff")
+                       if (cell->type.in(ID($_BUF_), ID($_NOT_)))
                        {
-                               // FIXME: use init property
-                               assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
+                               string op = cell->type == ID($_NOT_) ? "!" : "";
+                               definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)), op.c_str(), rvalue(cell->getPort(ID::A))));
                                continue;
                        }
 
-                       // FIXME: $_BUF_, $_NOT_, $_AND_, $_NAND_, $_OR_, $_NOR_,
-                       // $_XOR_, $_XNOR_, $_MUX_, $_AOI3_, $_OAI3_, $_AOI4_, $_OAI4_ 
+                       if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_)))
+                       {
+                               string op;
+
+                               if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_ANDNOT_))) op = "&";
+                               if (cell->type.in(ID($_OR_), ID($_NOR_), ID($_ORNOT_))) op = "|";
+                               if (cell->type.in(ID($_XOR_)))  op = "xor";
+                               if (cell->type.in(ID($_XNOR_)))  op = "xnor";
+
+                               if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
+                                       definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort(ID::Y)),
+                                                       rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
+                               else
+                               if (cell->type.in(ID($_NAND_), ID($_NOR_)))
+                                       definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort(ID::Y)),
+                                                       rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
+                               else
+                                       definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
+                                                       rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
+                               continue;
+                       }
+
+                       if (cell->type == ID($_MUX_))
+                       {
+                               definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort(ID::Y)),
+                                               rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
+                               continue;
+                       }
+
+                       if (cell->type == ID($_NMUX_))
+                       {
+                               definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort(ID::Y)),
+                                               rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
+                               continue;
+                       }
+
+                       if (cell->type == ID($_AOI3_))
+                       {
+                               definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort(ID::Y)),
+                                               rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
+                               continue;
+                       }
+
+                       if (cell->type == ID($_OAI3_))
+                       {
+                               definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort(ID::Y)),
+                                               rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
+                               continue;
+                       }
+
+                       if (cell->type == ID($_AOI4_))
+                       {
+                               definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort(ID::Y)),
+                                               rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
+                               continue;
+                       }
+
+                       if (cell->type == ID($_OAI4_))
+                       {
+                               definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort(ID::Y)),
+                                               rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
+                               continue;
+                       }
 
                        if (cell->type[0] == '$')
                                log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
 
-                       f << stringf("    %s : %s;\n", cid(cell->name), cid(cell->type));
+//                     f << stringf("    %s : %s;\n", cid(cell->name), cid(cell->type));
 
                        for (auto &conn : cell->connections())
                                if (cell->output(conn.first))
-                                       assignments.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
+                                       definitions.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
                                else
-                                       assignments.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
+                                       definitions.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
                }
 
-               for (auto &it : partial_assignments)
+               for (Wire *wire : partial_assignment_wires)
                {
-                       std::sort(it.second.begin(), it.second.end());
-
                        string expr;
-                       int offset = 0;
-                       for (auto rhs : it.second) {
+
+                       for (int i = 0; i < wire->width; i++)
+                       {
                                if (!expr.empty())
                                        expr = " :: " + expr;
-                               if (offset < rhs.offset)
-                                       expr = stringf(" :: 0ub%d_0 ", rhs.offset - offset) + expr;
-                               expr = rhs.rhs_expr + expr;
-                               offset = rhs.offset + rhs.width;
+
+                               if (partial_assignment_bits.count(sigmap(SigBit(wire, i))))
+                               {
+                                       int width = 1;
+                                       const auto &bit_a = partial_assignment_bits.at(sigmap(SigBit(wire, i)));
+
+                                       while (i+1 < wire->width)
+                                       {
+                                               SigBit next_bit = sigmap(SigBit(wire, i+1));
+
+                                               if (!partial_assignment_bits.count(next_bit))
+                                                       break;
+
+                                               const auto &bit_b = partial_assignment_bits.at(next_bit);
+                                               if (strcmp(bit_a.first, bit_b.first))
+                                                       break;
+                                               if (bit_a.second+width != bit_b.second)
+                                                       break;
+
+                                               width++, i++;
+                                       }
+
+                                       expr = stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second) + expr;
+                               }
+                               else if (sigmap(SigBit(wire, i)).wire == nullptr)
+                               {
+                                       string bits;
+                                       SigSpec sig = sigmap(SigSpec(wire, i));
+
+                                       while (i+1 < wire->width) {
+                                               SigBit next_bit = sigmap(SigBit(wire, i+1));
+                                               if (next_bit.wire != nullptr)
+                                                       break;
+                                               sig.append(next_bit);
+                                               i++;
+                                       }
+
+                                       for (int k = GetSize(sig)-1; k >= 0; k--)
+                                               bits += sig[k] == State::S1 ? '1' : '0';
+
+                                       expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr;
+                               }
+                               else if (sigmap(SigBit(wire, i)) == SigBit(wire, i))
+                               {
+                                       int length = 1;
+
+                                       while (i+1 < wire->width) {
+                                               if (partial_assignment_bits.count(sigmap(SigBit(wire, i+1))))
+                                                       break;
+                                               if (sigmap(SigBit(wire, i+1)) != SigBit(wire, i+1))
+                                                       break;
+                                               i++, length++;
+                                       }
+
+                                       expr = stringf("0ub%d_0", length) + expr;
+                               }
+                               else
+                               {
+                                       string bits;
+                                       SigSpec sig = sigmap(SigSpec(wire, i));
+
+                                       while (i+1 < wire->width) {
+                                               SigBit next_bit = sigmap(SigBit(wire, i+1));
+                                               if (next_bit.wire == nullptr || partial_assignment_bits.count(next_bit))
+                                                       break;
+                                               sig.append(next_bit);
+                                               i++;
+                                       }
+
+                                       expr = rvalue(sig) + expr;
+                               }
                        }
-                       if (offset < it.first->width)
-                               expr = stringf("0ub%d_0 :: ", it.first->width - offset) + expr;
-                       assignments.push_back(stringf("%s := %s;", cid(it.first->name), expr.c_str()));
+
+                       definitions.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
+               }
+
+               if (!inputvars.empty()) {
+                       f << stringf("  IVAR\n");
+                       for (const string &line : inputvars)
+                               f << stringf("    %s\n", line.c_str());
+               }
+
+               if (!vars.empty()) {
+                       f << stringf("  VAR\n");
+                       for (const string &line : vars)
+                               f << stringf("    %s\n", line.c_str());
                }
 
-               f << stringf("  ASSIGN\n");
-               for (const string &line : assignments)
-                       f << stringf("    %s\n", line.c_str());
+               if (!definitions.empty()) {
+                       f << stringf("  DEFINE\n");
+                       for (const string &line : definitions)
+                               f << stringf("    %s\n", line.c_str());
+               }
+
+               if (!assignments.empty()) {
+                       f << stringf("  ASSIGN\n");
+                       for (const string &line : assignments)
+                               f << stringf("    %s\n", line.c_str());
+               }
+
+               if (!invarspecs.empty()) {
+                       for (const string &line : invarspecs)
+                               f << stringf("  INVARSPEC %s\n", line.c_str());
+               }
        }
 };
 
 struct SmvBackend : public Backend {
        SmvBackend() : Backend("smv", "write design to SMV file") { }
-       virtual void help()
+       void help() override
        {
                //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
                log("\n");
@@ -434,12 +720,12 @@ struct SmvBackend : public Backend {
                log("THIS COMMAND IS UNDER CONSTRUCTION\n");
                log("\n");
        }
-       virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+       void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
        {
                std::ifstream template_f;
                bool verbose = false;
 
-               log_header("Executing SMV backend.\n");
+               log_header(design, "Executing SMV backend.\n");
 
                size_t argidx;
                for (argidx = 1; argidx < args.size(); argidx++)
@@ -461,7 +747,7 @@ struct SmvBackend : public Backend {
                pool<Module*> modules;
 
                for (auto module : design->modules())
-                       if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
+                       if (!module->get_blackbox_attribute() && !module->has_memories_warn() && !module->has_processes_warn())
                                modules.insert(module);
 
                if (template_f.is_open())
@@ -473,7 +759,7 @@ struct SmvBackend : public Backend {
                                while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
                                        indent++;
 
-                               if (line[indent] == '$')
+                               if (line[indent] == '%')
                                {
                                        vector<string> stmt = split_tokens(line);
 
@@ -483,6 +769,7 @@ struct SmvBackend : public Backend {
                                        if (GetSize(stmt) == 2 && stmt[0] == "%module")
                                        {
                                                Module *module = design->module(RTLIL::escape_id(stmt[1]));
+                                               modules.erase(module);
 
                                                if (module == nullptr)
                                                        log_error("Module '%s' not found.\n", stmt[1].c_str());
@@ -504,15 +791,18 @@ struct SmvBackend : public Backend {
                        }
                }
 
-               *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
+               if (!modules.empty())
+               {
+                       *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 
-               for (auto module : modules) {
-                       log("Creating SMV representation of module %s.\n", log_id(module));
-                       SmvWorker worker(module, verbose, *f);
-                       worker.run();
-               }
+                       for (auto module : modules) {
+                               log("Creating SMV representation of module %s.\n", log_id(module));
+                               SmvWorker worker(module, verbose, *f);
+                               worker.run();
+                       }
 
-               *f << stringf("-- end of yosys output\n");
+                       *f << stringf("-- end of yosys output\n");
+               }
 
                if (template_f.is_open()) {
                        std::string line;