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