backends/smv/smv.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #include "kernel/rtlil.h"
  21 #include "kernel/register.h"
  22 #include "kernel/sigtools.h"
  23 #include "kernel/celltypes.h"
  24 #include "kernel/log.h"
  25 #include <string>
  26
  27 USING_YOSYS_NAMESPACE
  28 PRIVATE_NAMESPACE_BEGIN
  29
  30 struct SmvWorker
  31 {
  32         CellTypes ct;
  33         SigMap sigmap;
  34         RTLIL::Module *module;
  35         std::ostream &f;
  36         bool verbose;
  37
  38         int idcounter;
  39         dict<IdString, shared_str> idcache;
  40         pool<shared_str> used_names;
  41         vector<shared_str> strbuf;
  42
  43         struct assign_rhs_chunk {
  44                 string rhs_expr;
  45                 int offset, width;
  46                 bool operator<(const assign_rhs_chunk &other) const { return offset < other.offset; }
  47         };
  48
  49         dict<Wire*, vector<assign_rhs_chunk>> partial_assignments;
  50         vector<string> assignments;
  51
  52         const char *cid()
  53         {
  54                 while (true) {
  55                         shared_str s(stringf("_%d", idcounter++));
  56                         if (!used_names.count(s)) {
  57                                 used_names.insert(s);
  58                                 return s.c_str();
  59                         }
  60                 }
  61         }
  62
  63         const char *cid(IdString id, bool precache = false)
  64         {
  65                 if (!idcache.count(id))
  66                 {
  67                         string name = stringf("_%s", id.c_str());
  68
  69                         if (name.substr(0, 2) == "_\\")
  70                                 name = "_" + name.substr(2);
  71
  72                         for (auto &c : name) {
  73                                 if (c == '|' || c == '$' || c == '_') continue;
  74                                 if (c >= 'a' && c <='z') continue;
  75                                 if (c >= 'A' && c <='Z') continue;
  76                                 if (c >= '0' && c <='9') continue;
  77                                 if (precache) return nullptr;
  78                                 c = '#';
  79                         }
  80
  81                         if (name == "_main")
  82                                 name = "main";
  83
  84                         while (used_names.count(name))
  85                                 name += "_";
  86
  87                         shared_str s(name);
  88                         used_names.insert(s);
  89                         idcache[id] = s;
  90                 }
  91
  92                 return idcache.at(id).c_str();
  93         }
  94
  95         SmvWorker(RTLIL::Module *module, bool verbose, std::ostream &f) :
  96                         ct(module->design), sigmap(module), module(module), f(f), verbose(verbose), idcounter(0)
  97         {
  98                 for (auto mod : module->design->modules())
  99                         cid(mod->name, true);
 100
 101                 for (auto wire : module->wires())
 102                         cid(wire->name, true);
 103
 104                 for (auto cell : module->cells()) {
 105                         cid(cell->name, true);
 106                         cid(cell->type, true);
 107                         for (auto &conn : cell->connections())
 108                                 cid(conn.first, true);
 109                 }
 110         }
 111
 112         const char *rvalue(SigSpec sig, bool skip_sigmap = false, int width = -1, bool is_signed = false)
 113         {
 114                 if (!skip_sigmap)
 115                         sigmap.apply(sig);
 116
 117                 string s;
 118                 int count_chunks = 0;
 119                 for (auto &c : sig.chunks()) {
 120                         count_chunks++;
 121                         if (!s.empty())
 122                                 s = " :: " + s;
 123                         if (c.wire) {
 124                                 if (c.offset != 0 || c.width != c.wire->width)
 125                                         s = stringf("%s[%d:%d]", cid(c.wire->name), c.offset+c.width-1, c.offset) + s;
 126                                 else
 127                                         s = cid(c.wire->name) + s;
 128                         } else {
 129                                 string v = stringf("0ub%d_", c.width);
 130                                 for (int i = c.width-1; i >= 0; i--)
 131                                         v += c.data.at(i) == State::S1 ? '1' : '0';
 132                                 s = v + s;
 133                         }
 134                 }
 135
 136                 if (width >= 0) {
 137                         if (is_signed) {
 138                                 if (GetSize(sig) > width)
 139                                         s = stringf("signed(resize(%s, %d))", s.c_str(), width);
 140                                 else
 141                                         s = stringf("resize(signed(%s), %d)", s.c_str(), width);
 142                         } else
 143                                 s = stringf("resize(%s, %d)", s.c_str(), width);
 144                 } else if (is_signed)
 145                         s = stringf("signed(%s)", s.c_str());
 146                 else if (count_chunks > 1)
 147                         s = stringf("(%s)", s.c_str());
 148
 149                 strbuf.push_back(s);
 150                 return strbuf.back().c_str();
 151         }
 152
 153         const char *rvalue_u(SigSpec sig, int width = -1)
 154         {
 155                 return rvalue(sig, false, width, false);
 156         }
 157
 158         const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true)
 159         {
 160                 return rvalue(sig, false, width, is_signed);
 161         }
 162
 163         const char *lvalue(SigSpec sig, bool skip_sigmap = false)
 164         {
 165                 if (!skip_sigmap)
 166                         sigmap.apply(sig);
 167
 168                 if (sig.is_wire())
 169                         return rvalue(sig, true);
 170
 171                 const char *temp_id = cid();
 172                 f << stringf("    %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig));
 173
 174                 int offset = 0;
 175                 for (auto &c : sig.chunks())
 176                 {
 177                         log_assert(c.wire != nullptr);
 178
 179                         assign_rhs_chunk rhs;
 180                         if (offset != 0 || c.width != GetSize(sig))
 181                                 rhs.rhs_expr = stringf("%s[%d:%d]", temp_id, offset+c.width-1, offset);
 182                         else
 183                                 rhs.rhs_expr = temp_id;
 184                         rhs.offset = c.offset;
 185                         rhs.width = c.width;
 186
 187                         partial_assignments[c.wire].push_back(rhs);
 188                         offset += c.width;
 189                 }
 190
 191                 return temp_id;
 192         }
 193
 194         void run()
 195         {
 196                 f << stringf("MODULE %s\n", cid(module->name));
 197                 f << stringf("  VAR\n");
 198
 199                 for (auto wire : module->wires())
 200                 {
 201                         SigSpec this_sig = wire, driver_sig = sigmap(wire);
 202                         SigSpec unused_bits_in_this_sig;
 203                         SigSpec driver_for_unused_bits;
 204
 205                         for (int i = 0; i < GetSize(this_sig); i++)
 206                                 if (this_sig[i] != driver_sig[i]) {
 207                                         unused_bits_in_this_sig.append(this_sig[i]);
 208                                         driver_for_unused_bits.append(driver_sig[i]);
 209                                 }
 210
 211                         if (GetSize(unused_bits_in_this_sig) == GetSize(this_sig))
 212                         {
 213                                 f << stringf("    -- unused -- %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
 214                         }
 215                         else
 216                         {
 217                                 f << stringf("    %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
 218
 219                                 if (!unused_bits_in_this_sig.empty())
 220                                         assignments.push_back(stringf("%s := 0ub%d_0; -- unused %s -- using %s instead", lvalue(unused_bits_in_this_sig, true),
 221                                                         GetSize(unused_bits_in_this_sig), log_signal(unused_bits_in_this_sig), log_signal(driver_for_unused_bits)));
 222                         }
 223                 }
 224
 225                 for (auto cell : module->cells())
 226                 {
 227                         // FIXME: $slice, $concat, $mem
 228
 229                         if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
 230                         {
 231                                 SigSpec sig_a = cell->getPort("\\A");
 232                                 SigSpec sig_b = cell->getPort("\\B");
 233
 234                                 int width_y = GetSize(cell->getPort("\\Y"));
 235                                 int shift_b_width = GetSize(sig_b);
 236                                 int width_ay = std::max(GetSize(sig_a), width_y);
 237                                 int width = width_ay;
 238
 239                                 for (int i = 1, j = 0;; i <<= 1, j++)
 240                                         if (width_ay < i) {
 241                                                 width = i-1;
 242                                                 shift_b_width = std::min(shift_b_width, j);
 243                                                 break;
 244                                         }
 245
 246                                 bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
 247                                 bool signed_b = cell->getParam("\\B_SIGNED").as_bool();
 248                                 string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
 249                                 string expr, expr_a;
 250
 251                                 if (cell->type == "$sshr" && signed_a)
 252                                 {
 253                                         expr_a = rvalue_s(sig_a, width);
 254                                         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);
 255                                         if (shift_b_width < GetSize(sig_b))
 256                                                 expr = stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s",
 257                                                                 rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
 258                                                                 rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
 259                                 }
 260                                 else if (cell->type.in("$shift", "$shiftx") && signed_b)
 261                                 {
 262                                         expr_a = rvalue_u(sig_a, width);
 263
 264                                         const char *b_shr = rvalue_u(sig_b);
 265                                         const char *b_shl = cid();
 266
 267                                         f << stringf("    %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b));
 268                                         assignments.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b)));
 269
 270                                         string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y);
 271                                         string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y);
 272
 273                                         if (shift_b_width < GetSize(sig_b)) {
 274                                                 expr_shl = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl, GetSize(sig_b)-1, shift_b_width,
 275                                                                 GetSize(sig_b)-shift_b_width, width_y, expr_shl.c_str());
 276                                                 expr_shr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr, GetSize(sig_b)-1, shift_b_width,
 277                                                                 GetSize(sig_b)-shift_b_width, width_y, expr_shr.c_str());
 278                                         }
 279
 280                                         expr = stringf("bool(%s) ? %s : %s", rvalue(sig_b[GetSize(sig_b)-1]), expr_shl.c_str(), expr_shr.c_str());
 281                                 }
 282                                 else
 283                                 {
 284                                         if (cell->type.in("$shift", "$shiftx") || !signed_a)
 285                                                 expr_a = rvalue_u(sig_a, width);
 286                                         else
 287                                                 expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
 288
 289                                         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);
 290                                         if (shift_b_width < GetSize(sig_b))
 291                                                 expr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b), GetSize(sig_b)-1, shift_b_width,
 292                                                                 GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
 293                                 }
 294
 295                                 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
 296
 297                                 continue;
 298                         }
 299
 300                         if (cell->type.in("$not", "$pos", "$neg"))
 301                         {
 302                                 int width = GetSize(cell->getPort("\\Y"));
 303                                 string expr_a, op;
 304
 305                                 if (cell->type == "$not")  op = "!";
 306                                 if (cell->type == "$pos")  op = "";
 307                                 if (cell->type == "$neg")  op = "-";
 308
 309                                 if (cell->getParam("\\A_SIGNED").as_bool())
 310                                 {
 311                                         assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
 312                                                         op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
 313                                 }
 314                                 else
 315                                 {
 316                                         assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
 317                                                         op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
 318                                 }
 319
 320                                 continue;
 321                         }
 322
 323                         if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
 324                         {
 325                                 int width = GetSize(cell->getPort("\\Y"));
 326                                 string expr_a, expr_b, op;
 327
 328                                 if (cell->type == "$add")  op = "+";
 329                                 if (cell->type == "$sub")  op = "-";
 330                                 if (cell->type == "$mul")  op = "*";
 331                                 if (cell->type == "$and")  op = "&";
 332                                 if (cell->type == "$or")   op = "|";
 333                                 if (cell->type == "$xor")  op = "xor";
 334                                 if (cell->type == "$xnor") op = "xnor";
 335
 336                                 if (cell->getParam("\\A_SIGNED").as_bool())
 337                                 {
 338                                         assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
 339                                                         rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
 340                                 }
 341                                 else
 342                                 {
 343                                         assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
 344                                                         rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
 345                                 }
 346
 347                                 continue;
 348                         }
 349
 350                         if (cell->type.in("$div", "$mod"))
 351                         {
 352                                 int width_y = GetSize(cell->getPort("\\Y"));
 353                                 int width = std::max(width_y, GetSize(cell->getPort("\\A")));
 354                                 width = std::max(width, GetSize(cell->getPort("\\B")));
 355                                 string expr_a, expr_b, op;
 356
 357                                 if (cell->type == "$div")  op = "/";
 358                                 if (cell->type == "$mod")  op = "mod";
 359
 360                                 if (cell->getParam("\\A_SIGNED").as_bool())
 361                                 {
 362                                         assignments.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
 363                                                         rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
 364                                 }
 365                                 else
 366                                 {
 367                                         assignments.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
 368                                                         rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
 369                                 }
 370
 371                                 continue;
 372                         }
 373
 374                         if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
 375                         {
 376                                 int width = std::max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
 377                                 string expr_a, expr_b, op;
 378
 379                                 if (cell->type == "$eq")  op = "=";
 380                                 if (cell->type == "$ne")  op = "!=";
 381                                 if (cell->type == "$eqx") op = "=";
 382                                 if (cell->type == "$nex") op = "!=";
 383                                 if (cell->type == "$lt")  op = "<";
 384                                 if (cell->type == "$le")  op = "<=";
 385                                 if (cell->type == "$ge")  op = ">=";
 386                                 if (cell->type == "$gt")  op = ">";
 387
 388                                 if (cell->getParam("\\A_SIGNED").as_bool())
 389                                 {
 390                                         expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
 391                                         expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
 392                                 }
 393                                 else
 394                                 {
 395                                         expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
 396                                         expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
 397                                 }
 398
 399                                 assignments.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
 400                                                 expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
 401
 402                                 continue;
 403                         }
 404
 405                         if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
 406                         {
 407                                 int width_a = GetSize(cell->getPort("\\A"));
 408                                 int width_y = GetSize(cell->getPort("\\Y"));
 409                                 const char *expr_a = rvalue(cell->getPort("\\A"));
 410                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 411                                 string expr;
 412
 413                                 if (cell->type == "$reduce_and")  expr = stringf("%s = !0ub%d_0", expr_a, width_a);
 414                                 if (cell->type == "$reduce_or")   expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 415                                 if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 416
 417                                 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 418                                 continue;
 419                         }
 420
 421                         if (cell->type.in("$reduce_xor", "$reduce_xnor"))
 422                         {
 423                                 int width_y = GetSize(cell->getPort("\\Y"));
 424                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 425                                 string expr;
 426
 427                                 for (auto bit : cell->getPort("\\A")) {
 428                                         if (!expr.empty())
 429                                                 expr += " xor ";
 430                                         expr += rvalue(bit);
 431                                 }
 432
 433                                 if (cell->type == "$reduce_xnor")
 434                                         expr = "!(" + expr + ")";
 435
 436                                 assignments.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
 437                                 continue;
 438                         }
 439
 440                         if (cell->type.in("$logic_and", "$logic_or"))
 441                         {
 442                                 int width_a = GetSize(cell->getPort("\\A"));
 443                                 int width_b = GetSize(cell->getPort("\\B"));
 444                                 int width_y = GetSize(cell->getPort("\\Y"));
 445
 446                                 string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
 447                                 string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
 448                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 449
 450                                 string expr;
 451                                 if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
 452                                 if (cell->type == "$logic_or")  expr = expr_a + " | " + expr_b;
 453
 454                                 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 455                                 continue;
 456                         }
 457
 458                         if (cell->type.in("$logic_not"))
 459                         {
 460                                 int width_a = GetSize(cell->getPort("\\A"));
 461                                 int width_y = GetSize(cell->getPort("\\Y"));
 462
 463                                 string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
 464                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 465
 466                                 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
 467                                 continue;
 468                         }
 469
 470                         if (cell->type.in("$mux", "$pmux"))
 471                         {
 472                                 int width = GetSize(cell->getPort("\\Y"));
 473                                 SigSpec sig_a = cell->getPort("\\A");
 474                                 SigSpec sig_b = cell->getPort("\\B");
 475                                 SigSpec sig_s = cell->getPort("\\S");
 476
 477                                 string expr;
 478                                 for (int i = 0; i < GetSize(sig_s); i++)
 479                                         expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
 480                                 expr += rvalue(sig_a);
 481
 482                                 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
 483                                 continue;
 484                         }
 485
 486                         if (cell->type == "$dff")
 487                         {
 488                                 // FIXME: use init property
 489                                 assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
 490                                 continue;
 491                         }
 492
 493                         if (cell->type.in("$_BUF_", "$_NOT_"))
 494                         {
 495                                 string op = cell->type == "$_NOT_" ? "!" : "";
 496                                 assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
 497                                 continue;
 498                         }
 499
 500                         if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
 501                         {
 502                                 string op;
 503
 504                                 if (cell->type.in("$_AND_", "$_NAND_")) op = "&";
 505                                 if (cell->type.in("$_OR_", "$_NOR_")) op = "|";
 506                                 if (cell->type.in("$_XOR_"))  op = "xor";
 507                                 if (cell->type.in("$_XNOR_"))  op = "xnor";
 508
 509                                 if (cell->type.in("$_NAND_", "$_NOR_"))
 510                                         assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
 511                                                         rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
 512                                 else
 513                                         assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
 514                                                         rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
 515                                 continue;
 516                         }
 517
 518                         if (cell->type == "$_MUX_")
 519                         {
 520                                 assignments.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
 521                                                 rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
 522                                 continue;
 523                         }
 524
 525                         if (cell->type == "$_AOI3_")
 526                         {
 527                                 assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
 528                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
 529                                 continue;
 530                         }
 531
 532                         if (cell->type == "$_OAI3_")
 533                         {
 534                                 assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
 535                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
 536                                 continue;
 537                         }
 538
 539                         if (cell->type == "$_AOI4_")
 540                         {
 541                                 assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
 542                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
 543                                 continue;
 544                         }
 545
 546                         if (cell->type == "$_OAI4_")
 547                         {
 548                                 assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
 549                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
 550                                 continue;
 551                         }
 552
 553                         if (cell->type[0] == '$')
 554                                 log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
 555
 556                         f << stringf("    %s : %s;\n", cid(cell->name), cid(cell->type));
 557
 558                         for (auto &conn : cell->connections())
 559                                 if (cell->output(conn.first))
 560                                         assignments.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
 561                                 else
 562                                         assignments.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
 563                 }
 564
 565                 for (auto &it : partial_assignments)
 566                 {
 567                         std::sort(it.second.begin(), it.second.end());
 568
 569                         string expr;
 570                         int offset = 0;
 571                         for (auto rhs : it.second) {
 572                                 if (!expr.empty())
 573                                         expr = " :: " + expr;
 574                                 if (offset < rhs.offset)
 575                                         expr = stringf(" :: 0ub%d_0 ", rhs.offset - offset) + expr;
 576                                 expr = rhs.rhs_expr + expr;
 577                                 offset = rhs.offset + rhs.width;
 578                         }
 579                         if (offset < it.first->width)
 580                                 expr = stringf("0ub%d_0 :: ", it.first->width - offset) + expr;
 581                         assignments.push_back(stringf("%s := %s;", cid(it.first->name), expr.c_str()));
 582                 }
 583
 584                 f << stringf("  ASSIGN\n");
 585                 for (const string &line : assignments)
 586                         f << stringf("    %s\n", line.c_str());
 587         }
 588 };
 589
 590 struct SmvBackend : public Backend {
 591         SmvBackend() : Backend("smv", "write design to SMV file") { }
 592         virtual void help()
 593         {
 594                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 595                 log("\n");
 596                 log("    write_smv [options] [filename]\n");
 597                 log("\n");
 598                 log("Write an SMV description of the current design.\n");
 599                 log("\n");
 600                 log("    -verbose\n");
 601                 log("        this will print the recursive walk used to export the modules.\n");
 602                 log("\n");
 603                 log("    -tpl <template_file>\n");
 604                 log("        use the given template file. the line containing only the token '%%%%'\n");
 605                 log("        is replaced with the regular output of this command.\n");
 606                 log("\n");
 607                 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
 608                 log("\n");
 609         }
 610         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 611         {
 612                 std::ifstream template_f;
 613                 bool verbose = false;
 614
 615                 log_header("Executing SMV backend.\n");
 616
 617                 size_t argidx;
 618                 for (argidx = 1; argidx < args.size(); argidx++)
 619                 {
 620                         if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
 621                                 template_f.open(args[++argidx]);
 622                                 if (template_f.fail())
 623                                         log_error("Can't open template file `%s'.\n", args[argidx].c_str());
 624                                 continue;
 625                         }
 626                         if (args[argidx] == "-verbose") {
 627                                 verbose = true;
 628                                 continue;
 629                         }
 630                         break;
 631                 }
 632                 extra_args(f, filename, args, argidx);
 633
 634                 pool<Module*> modules;
 635
 636                 for (auto module : design->modules())
 637                         if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
 638                                 modules.insert(module);
 639
 640                 if (template_f.is_open())
 641                 {
 642                         std::string line;
 643                         while (std::getline(template_f, line))
 644                         {
 645                                 int indent = 0;
 646                                 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
 647                                         indent++;
 648
 649                                 if (line[indent] == '%')
 650                                 {
 651                                         vector<string> stmt = split_tokens(line);
 652
 653                                         if (GetSize(stmt) == 1 && stmt[0] == "%%")
 654                                                 break;
 655
 656                                         if (GetSize(stmt) == 2 && stmt[0] == "%module")
 657                                         {
 658                                                 Module *module = design->module(RTLIL::escape_id(stmt[1]));
 659                                                 modules.erase(module);
 660
 661                                                 if (module == nullptr)
 662                                                         log_error("Module '%s' not found.\n", stmt[1].c_str());
 663
 664                                                 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 665
 666                                                 log("Creating SMV representation of module %s.\n", log_id(module));
 667                                                 SmvWorker worker(module, verbose, *f);
 668                                                 worker.run();
 669
 670                                                 *f << stringf("-- end of yosys output\n");
 671                                                 continue;
 672                                         }
 673
 674                                         log_error("Unknown template statement: '%s'", line.c_str() + indent);
 675                                 }
 676
 677                                 *f << line << std::endl;
 678                         }
 679                 }
 680
 681                 if (!modules.empty())
 682                 {
 683                         *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 684
 685                         for (auto module : modules) {
 686                                 log("Creating SMV representation of module %s.\n", log_id(module));
 687                                 SmvWorker worker(module, verbose, *f);
 688                                 worker.run();
 689                         }
 690
 691                         *f << stringf("-- end of yosys output\n");
 692                 }
 693
 694                 if (template_f.is_open()) {
 695                         std::string line;
 696                         while (std::getline(template_f, line))
 697                                 *f << line << std::endl;
 698                 }
 699         }
 700 } SmvBackend;
 701
 702 PRIVATE_NAMESPACE_END