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                 for (auto &c : sig.chunks()) {
 119                         if (!s.empty())
 120                                 s = " :: " + s;
 121                         if (c.wire) {
 122                                 if (c.offset != 0 || c.width != c.wire->width)
 123                                         s = stringf("%s[%d:%d]", cid(c.wire->name), c.offset+c.width-1, c.offset) + s;
 124                                 else
 125                                         s = cid(c.wire->name) + s;
 126                         } else {
 127                                 string v = stringf("0ub%d_", c.width);
 128                                 for (int i = c.width-1; i >= 0; i--)
 129                                         v += c.data.at(i) == State::S1 ? '1' : '0';
 130                                 s = v + s;
 131                         }
 132                 }
 133
 134                 if (width >= 0) {
 135                         if (is_signed) {
 136                                 if (GetSize(sig) > width)
 137                                         s = stringf("signed(resize(%s, %d))", s.c_str(), width);
 138                                 else
 139                                         s = stringf("resize(signed(%s), %d)", s.c_str(), width);
 140                         } else
 141                                 s = stringf("resize(%s, %d)", s.c_str(), width);
 142                 } else if (is_signed)
 143                         s = stringf("signed(%s)", s.c_str());
 144
 145                 strbuf.push_back(s);
 146                 return strbuf.back().c_str();
 147         }
 148
 149         const char *rvalue_u(SigSpec sig, int width = -1)
 150         {
 151                 return rvalue(sig, false, width, false);
 152         }
 153
 154         const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true)
 155         {
 156                 return rvalue(sig, false, width, is_signed);
 157         }
 158
 159         const char *lvalue(SigSpec sig, bool skip_sigmap = false)
 160         {
 161                 if (!skip_sigmap)
 162                         sigmap.apply(sig);
 163
 164                 if (sig.is_wire())
 165                         return rvalue(sig, true);
 166
 167                 const char *temp_id = cid();
 168                 f << stringf("    %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig));
 169
 170                 int offset = 0;
 171                 for (auto &c : sig.chunks())
 172                 {
 173                         log_assert(c.wire != nullptr);
 174
 175                         assign_rhs_chunk rhs;
 176                         if (offset != 0 || c.width != GetSize(sig))
 177                                 rhs.rhs_expr = stringf("%s[%d:%d]", temp_id, offset+c.width-1, offset);
 178                         else
 179                                 rhs.rhs_expr = temp_id;
 180                         rhs.offset = c.offset;
 181                         rhs.width = c.width;
 182
 183                         partial_assignments[c.wire].push_back(rhs);
 184                         offset += c.width;
 185                 }
 186
 187                 return temp_id;
 188         }
 189
 190         void run()
 191         {
 192                 f << stringf("MODULE %s\n", cid(module->name));
 193                 f << stringf("  VAR\n");
 194
 195                 for (auto wire : module->wires())
 196                 {
 197                         SigSpec this_sig = wire, driver_sig = sigmap(wire);
 198                         SigSpec unused_bits_in_this_sig;
 199                         SigSpec driver_for_unused_bits;
 200
 201                         for (int i = 0; i < GetSize(this_sig); i++)
 202                                 if (this_sig[i] != driver_sig[i]) {
 203                                         unused_bits_in_this_sig.append(this_sig[i]);
 204                                         driver_for_unused_bits.append(driver_sig[i]);
 205                                 }
 206
 207                         if (GetSize(unused_bits_in_this_sig) == GetSize(this_sig))
 208                         {
 209                                 f << stringf("    -- unused -- %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
 210                         }
 211                         else
 212                         {
 213                                 f << stringf("    %s : unsigned word[%d]; -- %s\n", cid(wire->name), wire->width, log_id(wire));
 214
 215                                 if (!unused_bits_in_this_sig.empty())
 216                                         assignments.push_back(stringf("%s := 0ub%d_0; -- unused %s -- using %s instead", lvalue(unused_bits_in_this_sig, true),
 217                                                         GetSize(unused_bits_in_this_sig), log_signal(unused_bits_in_this_sig), log_signal(driver_for_unused_bits)));
 218                         }
 219                 }
 220
 221                 for (auto cell : module->cells())
 222                 {
 223                         // FIXME: $slice, $concat, $mem
 224
 225                         if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
 226                         {
 227                                 int width_y = GetSize(cell->getPort("\\Y"));
 228                                 int width = std::max(GetSize(cell->getPort("\\A")), width_y);
 229                                 bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
 230                                 string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
 231                                 string expr, expr_a;
 232
 233                                 if (signed_a) {
 234                                         expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
 235                                 } else
 236                                         expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
 237
 238                                 if (cell->type == "$sshr" && signed_a) {
 239                                         expr = stringf("resize(%s %s %s, %d)", expr_a.c_str(), op.c_str(), rvalue(cell->getPort("\\B")), width_y);
 240                                 } else {
 241                                         if (signed_a)
 242                                                 expr_a = "unsigned(" + expr_a + ")";
 243                                         if (cell->type.in("$shift", "$shiftx") && cell->getParam("\\B_SIGNED").as_bool())
 244                                                 expr = stringf("resize(%s %s signed(%s), %d)", expr_a.c_str(), op.c_str(), rvalue(cell->getPort("\\B")), width_y);
 245                                         else
 246                                                 expr = stringf("resize(%s %s %s, %d)", expr_a.c_str(), op.c_str(), rvalue(cell->getPort("\\B")), width_y);
 247                                 }
 248
 249                                 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
 250
 251                                 continue;
 252                         }
 253
 254                         if (cell->type.in("$not", "$pos", "$neg"))
 255                         {
 256                                 int width = GetSize(cell->getPort("\\Y"));
 257                                 string expr_a, op;
 258
 259                                 if (cell->type == "$not")  op = "!";
 260                                 if (cell->type == "$pos")  op = "";
 261                                 if (cell->type == "$neg")  op = "-";
 262
 263                                 if (cell->getParam("\\A_SIGNED").as_bool())
 264                                 {
 265                                         assignments.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
 266                                                         op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
 267                                 }
 268                                 else
 269                                 {
 270                                         assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
 271                                                         op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
 272                                 }
 273
 274                                 continue;
 275                         }
 276
 277                         if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
 278                         {
 279                                 int width = GetSize(cell->getPort("\\Y"));
 280                                 string expr_a, expr_b, op;
 281
 282                                 if (cell->type == "$add")  op = "+";
 283                                 if (cell->type == "$sub")  op = "-";
 284                                 if (cell->type == "$mul")  op = "*";
 285                                 if (cell->type == "$and")  op = "&";
 286                                 if (cell->type == "$or")   op = "|";
 287                                 if (cell->type == "$xor")  op = "xor";
 288                                 if (cell->type == "$xnor") op = "xnor";
 289
 290                                 if (cell->getParam("\\A_SIGNED").as_bool())
 291                                 {
 292                                         assignments.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
 293                                                         rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
 294                                 }
 295                                 else
 296                                 {
 297                                         assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
 298                                                         rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
 299                                 }
 300
 301                                 continue;
 302                         }
 303
 304                         if (cell->type.in("$div", "$mod"))
 305                         {
 306                                 int width_y = GetSize(cell->getPort("\\Y"));
 307                                 int width = std::max(width_y, GetSize(cell->getPort("\\A")));
 308                                 width = std::max(width, GetSize(cell->getPort("\\B")));
 309                                 string expr_a, expr_b, op;
 310
 311                                 if (cell->type == "$div")  op = "/";
 312                                 if (cell->type == "$mod")  op = "mod";
 313
 314                                 if (cell->getParam("\\A_SIGNED").as_bool())
 315                                 {
 316                                         assignments.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
 317                                                         rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
 318                                 }
 319                                 else
 320                                 {
 321                                         assignments.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
 322                                                         rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
 323                                 }
 324
 325                                 continue;
 326                         }
 327
 328                         if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
 329                         {
 330                                 int width = std::max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
 331                                 string expr_a, expr_b, op;
 332
 333                                 if (cell->type == "$eq")  op = "=";
 334                                 if (cell->type == "$ne")  op = "!=";
 335                                 if (cell->type == "$eqx") op = "=";
 336                                 if (cell->type == "$nex") op = "!=";
 337                                 if (cell->type == "$lt")  op = "<";
 338                                 if (cell->type == "$le")  op = "<=";
 339                                 if (cell->type == "$ge")  op = ">=";
 340                                 if (cell->type == "$gt")  op = ">";
 341
 342                                 if (cell->getParam("\\A_SIGNED").as_bool())
 343                                 {
 344                                         expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
 345                                         expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
 346                                 }
 347                                 else
 348                                 {
 349                                         expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
 350                                         expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
 351                                 }
 352
 353                                 assignments.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
 354                                                 expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
 355
 356                                 continue;
 357                         }
 358
 359                         if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
 360                         {
 361                                 int width_a = GetSize(cell->getPort("\\A"));
 362                                 int width_y = GetSize(cell->getPort("\\Y"));
 363                                 const char *expr_a = rvalue(cell->getPort("\\A"));
 364                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 365                                 string expr;
 366
 367                                 if (cell->type == "$reduce_and")  expr = stringf("%s = !0ub%d_0", expr_a, width_a);
 368                                 if (cell->type == "$reduce_or")   expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 369                                 if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 370
 371                                 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 372                                 continue;
 373                         }
 374
 375                         if (cell->type.in("$reduce_xor", "$reduce_xnor"))
 376                         {
 377                                 int width_y = GetSize(cell->getPort("\\Y"));
 378                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 379                                 string expr;
 380
 381                                 for (auto bit : cell->getPort("\\A")) {
 382                                         if (!expr.empty())
 383                                                 expr += " xor ";
 384                                         expr += rvalue(bit);
 385                                 }
 386
 387                                 if (cell->type == "$reduce_xnor")
 388                                         expr = "!(" + expr + ")";
 389
 390                                 assignments.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
 391                                 continue;
 392                         }
 393
 394                         if (cell->type.in("$logic_and", "$logic_or"))
 395                         {
 396                                 int width_a = GetSize(cell->getPort("\\A"));
 397                                 int width_b = GetSize(cell->getPort("\\B"));
 398                                 int width_y = GetSize(cell->getPort("\\Y"));
 399
 400                                 string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
 401                                 string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
 402                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 403
 404                                 string expr;
 405                                 if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
 406                                 if (cell->type == "$logic_or")  expr = expr_a + " | " + expr_b;
 407
 408                                 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 409                                 continue;
 410                         }
 411
 412                         if (cell->type.in("$logic_not"))
 413                         {
 414                                 int width_a = GetSize(cell->getPort("\\A"));
 415                                 int width_y = GetSize(cell->getPort("\\Y"));
 416
 417                                 string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
 418                                 const char *expr_y = lvalue(cell->getPort("\\Y"));
 419
 420                                 assignments.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
 421                                 continue;
 422                         }
 423
 424                         if (cell->type.in("$mux", "$pmux"))
 425                         {
 426                                 int width = GetSize(cell->getPort("\\Y"));
 427                                 SigSpec sig_a = cell->getPort("\\A");
 428                                 SigSpec sig_b = cell->getPort("\\B");
 429                                 SigSpec sig_s = cell->getPort("\\S");
 430
 431                                 string expr;
 432                                 for (int i = 0; i < GetSize(sig_s); i++)
 433                                         expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
 434                                 expr += rvalue(sig_a);
 435
 436                                 assignments.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
 437                                 continue;
 438                         }
 439
 440                         if (cell->type == "$dff")
 441                         {
 442                                 // FIXME: use init property
 443                                 assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
 444                                 continue;
 445                         }
 446
 447                         if (cell->type.in("$_BUF_", "$_NOT_"))
 448                         {
 449                                 string op = cell->type == "$_NOT_" ? "!" : "";
 450                                 assignments.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
 451                                 continue;
 452                         }
 453
 454                         if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
 455                         {
 456                                 string op;
 457
 458                                 if (cell->type.in("$_AND_", "$_NAND_")) op = "&";
 459                                 if (cell->type.in("$_OR_", "$_NOR_")) op = "|";
 460                                 if (cell->type.in("$_XOR_"))  op = "xor";
 461                                 if (cell->type.in("$_XNOR_"))  op = "xnor";
 462
 463                                 if (cell->type.in("$_NAND_", "$_NOR_"))
 464                                         assignments.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
 465                                                         rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
 466                                 else
 467                                         assignments.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
 468                                                         rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
 469                                 continue;
 470                         }
 471
 472                         if (cell->type == "$_MUX_")
 473                         {
 474                                 assignments.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
 475                                                 rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
 476                                 continue;
 477                         }
 478
 479                         if (cell->type == "$_AOI3_")
 480                         {
 481                                 assignments.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
 482                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
 483                                 continue;
 484                         }
 485
 486                         if (cell->type == "$_OAI3_")
 487                         {
 488                                 assignments.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
 489                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
 490                                 continue;
 491                         }
 492
 493                         if (cell->type == "$_AOI4_")
 494                         {
 495                                 assignments.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
 496                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
 497                                 continue;
 498                         }
 499
 500                         if (cell->type == "$_OAI4_")
 501                         {
 502                                 assignments.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
 503                                                 rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
 504                                 continue;
 505                         }
 506
 507                         if (cell->type[0] == '$')
 508                                 log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
 509
 510                         f << stringf("    %s : %s;\n", cid(cell->name), cid(cell->type));
 511
 512                         for (auto &conn : cell->connections())
 513                                 if (cell->output(conn.first))
 514                                         assignments.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
 515                                 else
 516                                         assignments.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
 517                 }
 518
 519                 for (auto &it : partial_assignments)
 520                 {
 521                         std::sort(it.second.begin(), it.second.end());
 522
 523                         string expr;
 524                         int offset = 0;
 525                         for (auto rhs : it.second) {
 526                                 if (!expr.empty())
 527                                         expr = " :: " + expr;
 528                                 if (offset < rhs.offset)
 529                                         expr = stringf(" :: 0ub%d_0 ", rhs.offset - offset) + expr;
 530                                 expr = rhs.rhs_expr + expr;
 531                                 offset = rhs.offset + rhs.width;
 532                         }
 533                         if (offset < it.first->width)
 534                                 expr = stringf("0ub%d_0 :: ", it.first->width - offset) + expr;
 535                         assignments.push_back(stringf("%s := %s;", cid(it.first->name), expr.c_str()));
 536                 }
 537
 538                 f << stringf("  ASSIGN\n");
 539                 for (const string &line : assignments)
 540                         f << stringf("    %s\n", line.c_str());
 541         }
 542 };
 543
 544 struct SmvBackend : public Backend {
 545         SmvBackend() : Backend("smv", "write design to SMV file") { }
 546         virtual void help()
 547         {
 548                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 549                 log("\n");
 550                 log("    write_smv [options] [filename]\n");
 551                 log("\n");
 552                 log("Write an SMV description of the current design.\n");
 553                 log("\n");
 554                 log("    -verbose\n");
 555                 log("        this will print the recursive walk used to export the modules.\n");
 556                 log("\n");
 557                 log("    -tpl <template_file>\n");
 558                 log("        use the given template file. the line containing only the token '%%%%'\n");
 559                 log("        is replaced with the regular output of this command.\n");
 560                 log("\n");
 561                 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
 562                 log("\n");
 563         }
 564         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 565         {
 566                 std::ifstream template_f;
 567                 bool verbose = false;
 568
 569                 log_header("Executing SMV backend.\n");
 570
 571                 size_t argidx;
 572                 for (argidx = 1; argidx < args.size(); argidx++)
 573                 {
 574                         if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
 575                                 template_f.open(args[++argidx]);
 576                                 if (template_f.fail())
 577                                         log_error("Can't open template file `%s'.\n", args[argidx].c_str());
 578                                 continue;
 579                         }
 580                         if (args[argidx] == "-verbose") {
 581                                 verbose = true;
 582                                 continue;
 583                         }
 584                         break;
 585                 }
 586                 extra_args(f, filename, args, argidx);
 587
 588                 pool<Module*> modules;
 589
 590                 for (auto module : design->modules())
 591                         if (!module->get_bool_attribute("\\blackbox") && !module->has_memories_warn() && !module->has_processes_warn())
 592                                 modules.insert(module);
 593
 594                 if (template_f.is_open())
 595                 {
 596                         std::string line;
 597                         while (std::getline(template_f, line))
 598                         {
 599                                 int indent = 0;
 600                                 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
 601                                         indent++;
 602
 603                                 if (line[indent] == '%')
 604                                 {
 605                                         vector<string> stmt = split_tokens(line);
 606
 607                                         if (GetSize(stmt) == 1 && stmt[0] == "%%")
 608                                                 break;
 609
 610                                         if (GetSize(stmt) == 2 && stmt[0] == "%module")
 611                                         {
 612                                                 Module *module = design->module(RTLIL::escape_id(stmt[1]));
 613                                                 modules.erase(module);
 614
 615                                                 if (module == nullptr)
 616                                                         log_error("Module '%s' not found.\n", stmt[1].c_str());
 617
 618                                                 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 619
 620                                                 log("Creating SMV representation of module %s.\n", log_id(module));
 621                                                 SmvWorker worker(module, verbose, *f);
 622                                                 worker.run();
 623
 624                                                 *f << stringf("-- end of yosys output\n");
 625                                                 continue;
 626                                         }
 627
 628                                         log_error("Unknown template statement: '%s'", line.c_str() + indent);
 629                                 }
 630
 631                                 *f << line << std::endl;
 632                         }
 633                 }
 634
 635                 if (!modules.empty())
 636                 {
 637                         *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 638
 639                         for (auto module : modules) {
 640                                 log("Creating SMV representation of module %s.\n", log_id(module));
 641                                 SmvWorker worker(module, verbose, *f);
 642                                 worker.run();
 643                         }
 644
 645                         *f << stringf("-- end of yosys output\n");
 646                 }
 647
 648                 if (template_f.is_open()) {
 649                         std::string line;
 650                         while (std::getline(template_f, line))
 651                                 *f << line << std::endl;
 652                 }
 653         }
 654 } SmvBackend;
 655
 656 PRIVATE_NAMESPACE_END