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         pool<Wire*> partial_assignment_wires;
  44         dict<SigBit, std::pair<const char*, int>> partial_assignment_bits;
  45         vector<string> inputvars, vars, definitions, assignments, invarspecs;
  46
  47         const char *cid()
  48         {
  49                 while (true) {
  50                         shared_str s(stringf("_%d", idcounter++));
  51                         if (!used_names.count(s)) {
  52                                 used_names.insert(s);
  53                                 return s.c_str();
  54                         }
  55                 }
  56         }
  57
  58         const char *cid(IdString id, bool precache = false)
  59         {
  60                 if (!idcache.count(id))
  61                 {
  62                         string name = stringf("_%s", id.c_str());
  63
  64                         if (name.compare(0, 2, "_\\") == 0)
  65                                 name = "_" + name.substr(2);
  66
  67                         for (auto &c : name) {
  68                                 if (c == '|' || c == '$' || c == '_') continue;
  69                                 if (c >= 'a' && c <='z') continue;
  70                                 if (c >= 'A' && c <='Z') continue;
  71                                 if (c >= '0' && c <='9') continue;
  72                                 if (precache) return nullptr;
  73                                 c = '#';
  74                         }
  75
  76                         if (name == "_main")
  77                                 name = "main";
  78
  79                         while (used_names.count(name))
  80                                 name += "_";
  81
  82                         shared_str s(name);
  83                         used_names.insert(s);
  84                         idcache[id] = s;
  85                 }
  86
  87                 return idcache.at(id).c_str();
  88         }
  89
  90         SmvWorker(RTLIL::Module *module, bool verbose, std::ostream &f) :
  91                         ct(module->design), sigmap(module), module(module), f(f), verbose(verbose), idcounter(0)
  92         {
  93                 for (auto mod : module->design->modules())
  94                         cid(mod->name, true);
  95
  96                 for (auto wire : module->wires())
  97                         cid(wire->name, true);
  98
  99                 for (auto cell : module->cells()) {
 100                         cid(cell->name, true);
 101                         cid(cell->type, true);
 102                         for (auto &conn : cell->connections())
 103                                 cid(conn.first, true);
 104                 }
 105         }
 106
 107         const char *rvalue(SigSpec sig, int width = -1, bool is_signed = false)
 108         {
 109                 string s;
 110                 int count_chunks = 0;
 111                 sigmap.apply(sig);
 112
 113                 for (int i = 0; i < GetSize(sig); i++)
 114                         if (partial_assignment_bits.count(sig[i]))
 115                         {
 116                                 int width = 1;
 117                                 const auto &bit_a = partial_assignment_bits.at(sig[i]);
 118
 119                                 while (i+width < GetSize(sig))
 120                                 {
 121                                         if (!partial_assignment_bits.count(sig[i+width]))
 122                                                 break;
 123
 124                                         const auto &bit_b = partial_assignment_bits.at(sig[i+width]);
 125                                         if (strcmp(bit_a.first, bit_b.first))
 126                                                 break;
 127                                         if (bit_a.second+width != bit_b.second)
 128                                                 break;
 129
 130                                         width++;
 131                                 }
 132
 133                                 if (i+width < GetSize(sig))
 134                                         s = stringf("%s :: ", rvalue(sig.extract(i+width, GetSize(sig)-(width+i))));
 135
 136                                 s += stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second);
 137
 138                                 if (i > 0)
 139                                         s += stringf(" :: %s", rvalue(sig.extract(0, i)));
 140
 141                                 count_chunks = 3;
 142                                 goto continue_with_resize;
 143                         }
 144
 145                 for (auto &c : sig.chunks()) {
 146                         count_chunks++;
 147                         if (!s.empty())
 148                                 s = " :: " + s;
 149                         if (c.wire) {
 150                                 if (c.offset != 0 || c.width != c.wire->width)
 151                                         s = stringf("%s[%d:%d]", cid(c.wire->name), c.offset+c.width-1, c.offset) + s;
 152                                 else
 153                                         s = cid(c.wire->name) + s;
 154                         } else {
 155                                 string v = stringf("0ub%d_", c.width);
 156                                 for (int i = c.width-1; i >= 0; i--)
 157                                         v += c.data.at(i) == State::S1 ? '1' : '0';
 158                                 s = v + s;
 159                         }
 160                 }
 161
 162         continue_with_resize:;
 163                 if (width >= 0) {
 164                         if (is_signed) {
 165                                 if (GetSize(sig) > width)
 166                                         s = stringf("signed(resize(%s, %d))", s.c_str(), width);
 167                                 else
 168                                         s = stringf("resize(signed(%s), %d)", s.c_str(), width);
 169                         } else
 170                                 s = stringf("resize(%s, %d)", s.c_str(), width);
 171                 } else if (is_signed)
 172                         s = stringf("signed(%s)", s.c_str());
 173                 else if (count_chunks > 1)
 174                         s = stringf("(%s)", s.c_str());
 175
 176                 strbuf.push_back(s);
 177                 return strbuf.back().c_str();
 178         }
 179
 180         const char *rvalue_u(SigSpec sig, int width = -1)
 181         {
 182                 return rvalue(sig, width, false);
 183         }
 184
 185         const char *rvalue_s(SigSpec sig, int width = -1, bool is_signed = true)
 186         {
 187                 return rvalue(sig, width, is_signed);
 188         }
 189
 190         const char *lvalue(SigSpec sig)
 191         {
 192                 sigmap.apply(sig);
 193
 194                 if (sig.is_wire())
 195                         return rvalue(sig);
 196
 197                 const char *temp_id = cid();
 198 //              f << stringf("    %s : unsigned word[%d]; -- %s\n", temp_id, GetSize(sig), log_signal(sig));
 199
 200                 int offset = 0;
 201                 for (auto bit : sig) {
 202                         log_assert(bit.wire != nullptr);
 203                         partial_assignment_wires.insert(bit.wire);
 204                         partial_assignment_bits[bit] = std::pair<const char*, int>(temp_id, offset++);
 205                 }
 206
 207                 return temp_id;
 208         }
 209
 210         void run()
 211         {
 212                 f << stringf("MODULE %s\n", cid(module->name));
 213
 214                 for (auto wire : module->wires())
 215                 {
 216                         if (SigSpec(wire) != sigmap(wire))
 217                                 partial_assignment_wires.insert(wire);
 218
 219                         if (wire->port_input)
 220                                 inputvars.push_back(stringf("%s : unsigned word[%d]; -- %s", cid(wire->name), wire->width, log_id(wire)));
 221
 222                         if (wire->attributes.count(ID::init))
 223                                 assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at(ID::init))));
 224                 }
 225
 226                 for (auto cell : module->cells())
 227                 {
 228                         // FIXME: $slice, $concat, $mem
 229
 230                         if (cell->type.in(ID($assert)))
 231                         {
 232                                 SigSpec sig_a = cell->getPort(ID::A);
 233                                 SigSpec sig_en = cell->getPort(ID::EN);
 234
 235                                 invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a)));
 236
 237                                 continue;
 238                         }
 239
 240                         if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
 241                         {
 242                                 SigSpec sig_a = cell->getPort(ID::A);
 243                                 SigSpec sig_b = cell->getPort(ID::B);
 244
 245                                 int width_y = GetSize(cell->getPort(ID::Y));
 246                                 int shift_b_width = GetSize(sig_b);
 247                                 int width_ay = max(GetSize(sig_a), width_y);
 248                                 int width = width_ay;
 249
 250                                 for (int i = 1, j = 0;; i <<= 1, j++)
 251                                         if (width_ay < i) {
 252                                                 width = i-1;
 253                                                 shift_b_width = min(shift_b_width, j);
 254                                                 break;
 255                                         }
 256
 257                                 bool signed_a = cell->getParam(ID::A_SIGNED).as_bool();
 258                                 bool signed_b = cell->getParam(ID::B_SIGNED).as_bool();
 259                                 string op = cell->type.in(ID($shl), ID($sshl)) ? "<<" : ">>";
 260                                 string expr, expr_a;
 261
 262                                 if (cell->type == ID($sshr) && signed_a)
 263                                 {
 264                                         expr_a = rvalue_s(sig_a, width);
 265                                         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);
 266                                         if (shift_b_width < GetSize(sig_b))
 267                                                 expr = stringf("%s != 0ud%d_0 ? (bool(%s) ? !0ud%d_0 : 0ud%d_0) : %s",
 268                                                                 rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
 269                                                                 rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
 270                                 }
 271                                 else if (cell->type.in(ID($shift), ID($shiftx)) && signed_b)
 272                                 {
 273                                         expr_a = rvalue_u(sig_a, width);
 274
 275                                         const char *b_shr = rvalue_u(sig_b);
 276                                         const char *b_shl = cid();
 277
 278 //                                      f << stringf("    %s : unsigned word[%d]; -- neg(%s)\n", b_shl, GetSize(sig_b), log_signal(sig_b));
 279                                         definitions.push_back(stringf("%s := unsigned(-%s);", b_shl, rvalue_s(sig_b)));
 280
 281                                         string expr_shl = stringf("resize(%s << %s[%d:0], %d)", expr_a.c_str(), b_shl, shift_b_width-1, width_y);
 282                                         string expr_shr = stringf("resize(%s >> %s[%d:0], %d)", expr_a.c_str(), b_shr, shift_b_width-1, width_y);
 283
 284                                         if (shift_b_width < GetSize(sig_b)) {
 285                                                 expr_shl = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shl, GetSize(sig_b)-1, shift_b_width,
 286                                                                 GetSize(sig_b)-shift_b_width, width_y, expr_shl.c_str());
 287                                                 expr_shr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", b_shr, GetSize(sig_b)-1, shift_b_width,
 288                                                                 GetSize(sig_b)-shift_b_width, width_y, expr_shr.c_str());
 289                                         }
 290
 291                                         expr = stringf("bool(%s) ? %s : %s", rvalue(sig_b[GetSize(sig_b)-1]), expr_shl.c_str(), expr_shr.c_str());
 292                                 }
 293                                 else
 294                                 {
 295                                         if (cell->type.in(ID($shift), ID($shiftx)) || !signed_a)
 296                                                 expr_a = rvalue_u(sig_a, width);
 297                                         else
 298                                                 expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
 299
 300                                         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);
 301                                         if (shift_b_width < GetSize(sig_b))
 302                                                 expr = stringf("%s[%d:%d] != 0ud%d_0 ? 0ud%d_0 : %s", rvalue_u(sig_b), GetSize(sig_b)-1, shift_b_width,
 303                                                                 GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
 304                                 }
 305
 306                                 definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
 307
 308                                 continue;
 309                         }
 310
 311                         if (cell->type.in(ID($not), ID($pos), ID($neg)))
 312                         {
 313                                 int width = GetSize(cell->getPort(ID::Y));
 314                                 string expr_a, op;
 315
 316                                 if (cell->type == ID($not))  op = "!";
 317                                 if (cell->type == ID($pos))  op = "";
 318                                 if (cell->type == ID($neg))  op = "-";
 319
 320                                 if (cell->getParam(ID::A_SIGNED).as_bool())
 321                                 {
 322                                         definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort(ID::Y)),
 323                                                         op.c_str(), rvalue_s(cell->getPort(ID::A), width)));
 324                                 }
 325                                 else
 326                                 {
 327                                         definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)),
 328                                                         op.c_str(), rvalue_u(cell->getPort(ID::A), width)));
 329                                 }
 330
 331                                 continue;
 332                         }
 333
 334                         if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor)))
 335                         {
 336                                 int width = GetSize(cell->getPort(ID::Y));
 337                                 string expr_a, expr_b, op;
 338
 339                                 if (cell->type == ID($add))  op = "+";
 340                                 if (cell->type == ID($sub))  op = "-";
 341                                 if (cell->type == ID($mul))  op = "*";
 342                                 if (cell->type == ID($and))  op = "&";
 343                                 if (cell->type == ID($or))   op = "|";
 344                                 if (cell->type == ID($xor))  op = "xor";
 345                                 if (cell->type == ID($xnor)) op = "xnor";
 346
 347                                 if (cell->getParam(ID::A_SIGNED).as_bool())
 348                                 {
 349                                         definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort(ID::Y)),
 350                                                         rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width)));
 351                                 }
 352                                 else
 353                                 {
 354                                         definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
 355                                                         rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width)));
 356                                 }
 357
 358                                 continue;
 359                         }
 360
 361                         // SMV has a "mod" operator, but its semantics don't seem to be well-defined - to be safe, don't generate it at all
 362                         if (cell->type.in(ID($div)/*, ID($mod), ID($modfloor)*/))
 363                         {
 364                                 int width_y = GetSize(cell->getPort(ID::Y));
 365                                 int width = max(width_y, GetSize(cell->getPort(ID::A)));
 366                                 width = max(width, GetSize(cell->getPort(ID::B)));
 367                                 string expr_a, expr_b, op;
 368
 369                                 if (cell->type == ID($div))  op = "/";
 370                                 //if (cell->type == ID($mod))  op = "mod";
 371
 372                                 if (cell->getParam(ID::A_SIGNED).as_bool())
 373                                 {
 374                                         definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
 375                                                         rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width), width_y));
 376                                 }
 377                                 else
 378                                 {
 379                                         definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort(ID::Y)),
 380                                                         rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width), width_y));
 381                                 }
 382
 383                                 continue;
 384                         }
 385
 386                         if (cell->type.in(ID($eq), ID($ne), ID($eqx), ID($nex), ID($lt), ID($le), ID($ge), ID($gt)))
 387                         {
 388                                 int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B)));
 389                                 string expr_a, expr_b, op;
 390
 391                                 if (cell->type == ID($eq))  op = "=";
 392                                 if (cell->type == ID($ne))  op = "!=";
 393                                 if (cell->type == ID($eqx)) op = "=";
 394                                 if (cell->type == ID($nex)) op = "!=";
 395                                 if (cell->type == ID($lt))  op = "<";
 396                                 if (cell->type == ID($le))  op = "<=";
 397                                 if (cell->type == ID($ge))  op = ">=";
 398                                 if (cell->type == ID($gt))  op = ">";
 399
 400                                 if (cell->getParam(ID::A_SIGNED).as_bool())
 401                                 {
 402                                         expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::A)), width);
 403                                         expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::B)), width);
 404                                 }
 405                                 else
 406                                 {
 407                                         expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::A)), width);
 408                                         expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::B)), width);
 409                                 }
 410
 411                                 definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
 412                                                 expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort(ID::Y))));
 413
 414                                 continue;
 415                         }
 416
 417                         if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)))
 418                         {
 419                                 int width_a = GetSize(cell->getPort(ID::A));
 420                                 int width_y = GetSize(cell->getPort(ID::Y));
 421                                 const char *expr_a = rvalue(cell->getPort(ID::A));
 422                                 const char *expr_y = lvalue(cell->getPort(ID::Y));
 423                                 string expr;
 424
 425                                 if (cell->type == ID($reduce_and))  expr = stringf("%s = !0ub%d_0", expr_a, width_a);
 426                                 if (cell->type == ID($reduce_or))   expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 427                                 if (cell->type == ID($reduce_bool)) expr = stringf("%s != 0ub%d_0", expr_a, width_a);
 428
 429                                 definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 430                                 continue;
 431                         }
 432
 433                         if (cell->type.in(ID($reduce_xor), ID($reduce_xnor)))
 434                         {
 435                                 int width_y = GetSize(cell->getPort(ID::Y));
 436                                 const char *expr_y = lvalue(cell->getPort(ID::Y));
 437                                 string expr;
 438
 439                                 for (auto bit : cell->getPort(ID::A)) {
 440                                         if (!expr.empty())
 441                                                 expr += " xor ";
 442                                         expr += rvalue(bit);
 443                                 }
 444
 445                                 if (cell->type == ID($reduce_xnor))
 446                                         expr = "!(" + expr + ")";
 447
 448                                 definitions.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
 449                                 continue;
 450                         }
 451
 452                         if (cell->type.in(ID($logic_and), ID($logic_or)))
 453                         {
 454                                 int width_a = GetSize(cell->getPort(ID::A));
 455                                 int width_b = GetSize(cell->getPort(ID::B));
 456                                 int width_y = GetSize(cell->getPort(ID::Y));
 457
 458                                 string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
 459                                 string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::B)), width_b);
 460                                 const char *expr_y = lvalue(cell->getPort(ID::Y));
 461
 462                                 string expr;
 463                                 if (cell->type == ID($logic_and)) expr = expr_a + " & " + expr_b;
 464                                 if (cell->type == ID($logic_or))  expr = expr_a + " | " + expr_b;
 465
 466                                 definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
 467                                 continue;
 468                         }
 469
 470                         if (cell->type.in(ID($logic_not)))
 471                         {
 472                                 int width_a = GetSize(cell->getPort(ID::A));
 473                                 int width_y = GetSize(cell->getPort(ID::Y));
 474
 475                                 string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
 476                                 const char *expr_y = lvalue(cell->getPort(ID::Y));
 477
 478                                 definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
 479                                 continue;
 480                         }
 481
 482                         if (cell->type.in(ID($mux), ID($pmux)))
 483                         {
 484                                 int width = GetSize(cell->getPort(ID::Y));
 485                                 SigSpec sig_a = cell->getPort(ID::A);
 486                                 SigSpec sig_b = cell->getPort(ID::B);
 487                                 SigSpec sig_s = cell->getPort(ID::S);
 488
 489                                 string expr;
 490                                 for (int i = 0; i < GetSize(sig_s); i++)
 491                                         expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
 492                                 expr += rvalue(sig_a);
 493
 494                                 definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
 495                                 continue;
 496                         }
 497
 498                         if (cell->type == ID($dff))
 499                         {
 500                                 vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort(ID::Q)), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))));
 501                                 assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort(ID::Q)), rvalue(cell->getPort(ID::D))));
 502                                 continue;
 503                         }
 504
 505                         if (cell->type.in(ID($_BUF_), ID($_NOT_)))
 506                         {
 507                                 string op = cell->type == ID($_NOT_) ? "!" : "";
 508                                 definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)), op.c_str(), rvalue(cell->getPort(ID::A))));
 509                                 continue;
 510                         }
 511
 512                         if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_)))
 513                         {
 514                                 string op;
 515
 516                                 if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_ANDNOT_))) op = "&";
 517                                 if (cell->type.in(ID($_OR_), ID($_NOR_), ID($_ORNOT_))) op = "|";
 518                                 if (cell->type.in(ID($_XOR_)))  op = "xor";
 519                                 if (cell->type.in(ID($_XNOR_)))  op = "xnor";
 520
 521                                 if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
 522                                         definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort(ID::Y)),
 523                                                         rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
 524                                 else
 525                                 if (cell->type.in(ID($_NAND_), ID($_NOR_)))
 526                                         definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort(ID::Y)),
 527                                                         rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
 528                                 else
 529                                         definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
 530                                                         rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
 531                                 continue;
 532                         }
 533
 534                         if (cell->type == ID($_MUX_))
 535                         {
 536                                 definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort(ID::Y)),
 537                                                 rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
 538                                 continue;
 539                         }
 540
 541                         if (cell->type == ID($_NMUX_))
 542                         {
 543                                 definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort(ID::Y)),
 544                                                 rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
 545                                 continue;
 546                         }
 547
 548                         if (cell->type == ID($_AOI3_))
 549                         {
 550                                 definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort(ID::Y)),
 551                                                 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
 552                                 continue;
 553                         }
 554
 555                         if (cell->type == ID($_OAI3_))
 556                         {
 557                                 definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort(ID::Y)),
 558                                                 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
 559                                 continue;
 560                         }
 561
 562                         if (cell->type == ID($_AOI4_))
 563                         {
 564                                 definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort(ID::Y)),
 565                                                 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
 566                                 continue;
 567                         }
 568
 569                         if (cell->type == ID($_OAI4_))
 570                         {
 571                                 definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort(ID::Y)),
 572                                                 rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
 573                                 continue;
 574                         }
 575
 576                         if (cell->type[0] == '$')
 577                                 log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell));
 578
 579 //                      f << stringf("    %s : %s;\n", cid(cell->name), cid(cell->type));
 580
 581                         for (auto &conn : cell->connections())
 582                                 if (cell->output(conn.first))
 583                                         definitions.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
 584                                 else
 585                                         definitions.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
 586                 }
 587
 588                 for (Wire *wire : partial_assignment_wires)
 589                 {
 590                         string expr;
 591
 592                         for (int i = 0; i < wire->width; i++)
 593                         {
 594                                 if (!expr.empty())
 595                                         expr = " :: " + expr;
 596
 597                                 if (partial_assignment_bits.count(sigmap(SigBit(wire, i))))
 598                                 {
 599                                         int width = 1;
 600                                         const auto &bit_a = partial_assignment_bits.at(sigmap(SigBit(wire, i)));
 601
 602                                         while (i+1 < wire->width)
 603                                         {
 604                                                 SigBit next_bit = sigmap(SigBit(wire, i+1));
 605
 606                                                 if (!partial_assignment_bits.count(next_bit))
 607                                                         break;
 608
 609                                                 const auto &bit_b = partial_assignment_bits.at(next_bit);
 610                                                 if (strcmp(bit_a.first, bit_b.first))
 611                                                         break;
 612                                                 if (bit_a.second+width != bit_b.second)
 613                                                         break;
 614
 615                                                 width++, i++;
 616                                         }
 617
 618                                         expr = stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second) + expr;
 619                                 }
 620                                 else if (sigmap(SigBit(wire, i)).wire == nullptr)
 621                                 {
 622                                         string bits;
 623                                         SigSpec sig = sigmap(SigSpec(wire, i));
 624
 625                                         while (i+1 < wire->width) {
 626                                                 SigBit next_bit = sigmap(SigBit(wire, i+1));
 627                                                 if (next_bit.wire != nullptr)
 628                                                         break;
 629                                                 sig.append(next_bit);
 630                                                 i++;
 631                                         }
 632
 633                                         for (int k = GetSize(sig)-1; k >= 0; k--)
 634                                                 bits += sig[k] == State::S1 ? '1' : '0';
 635
 636                                         expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr;
 637                                 }
 638                                 else if (sigmap(SigBit(wire, i)) == SigBit(wire, i))
 639                                 {
 640                                         int length = 1;
 641
 642                                         while (i+1 < wire->width) {
 643                                                 if (partial_assignment_bits.count(sigmap(SigBit(wire, i+1))))
 644                                                         break;
 645                                                 if (sigmap(SigBit(wire, i+1)) != SigBit(wire, i+1))
 646                                                         break;
 647                                                 i++, length++;
 648                                         }
 649
 650                                         expr = stringf("0ub%d_0", length) + expr;
 651                                 }
 652                                 else
 653                                 {
 654                                         string bits;
 655                                         SigSpec sig = sigmap(SigSpec(wire, i));
 656
 657                                         while (i+1 < wire->width) {
 658                                                 SigBit next_bit = sigmap(SigBit(wire, i+1));
 659                                                 if (next_bit.wire == nullptr || partial_assignment_bits.count(next_bit))
 660                                                         break;
 661                                                 sig.append(next_bit);
 662                                                 i++;
 663                                         }
 664
 665                                         expr = rvalue(sig) + expr;
 666                                 }
 667                         }
 668
 669                         definitions.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
 670                 }
 671
 672                 if (!inputvars.empty()) {
 673                         f << stringf("  IVAR\n");
 674                         for (const string &line : inputvars)
 675                                 f << stringf("    %s\n", line.c_str());
 676                 }
 677
 678                 if (!vars.empty()) {
 679                         f << stringf("  VAR\n");
 680                         for (const string &line : vars)
 681                                 f << stringf("    %s\n", line.c_str());
 682                 }
 683
 684                 if (!definitions.empty()) {
 685                         f << stringf("  DEFINE\n");
 686                         for (const string &line : definitions)
 687                                 f << stringf("    %s\n", line.c_str());
 688                 }
 689
 690                 if (!assignments.empty()) {
 691                         f << stringf("  ASSIGN\n");
 692                         for (const string &line : assignments)
 693                                 f << stringf("    %s\n", line.c_str());
 694                 }
 695
 696                 if (!invarspecs.empty()) {
 697                         for (const string &line : invarspecs)
 698                                 f << stringf("  INVARSPEC %s\n", line.c_str());
 699                 }
 700         }
 701 };
 702
 703 struct SmvBackend : public Backend {
 704         SmvBackend() : Backend("smv", "write design to SMV file") { }
 705         void help() override
 706         {
 707                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 708                 log("\n");
 709                 log("    write_smv [options] [filename]\n");
 710                 log("\n");
 711                 log("Write an SMV description of the current design.\n");
 712                 log("\n");
 713                 log("    -verbose\n");
 714                 log("        this will print the recursive walk used to export the modules.\n");
 715                 log("\n");
 716                 log("    -tpl <template_file>\n");
 717                 log("        use the given template file. the line containing only the token '%%%%'\n");
 718                 log("        is replaced with the regular output of this command.\n");
 719                 log("\n");
 720                 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
 721                 log("\n");
 722         }
 723         void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
 724         {
 725                 std::ifstream template_f;
 726                 bool verbose = false;
 727
 728                 log_header(design, "Executing SMV backend.\n");
 729
 730                 size_t argidx;
 731                 for (argidx = 1; argidx < args.size(); argidx++)
 732                 {
 733                         if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
 734                                 template_f.open(args[++argidx]);
 735                                 if (template_f.fail())
 736                                         log_error("Can't open template file `%s'.\n", args[argidx].c_str());
 737                                 continue;
 738                         }
 739                         if (args[argidx] == "-verbose") {
 740                                 verbose = true;
 741                                 continue;
 742                         }
 743                         break;
 744                 }
 745                 extra_args(f, filename, args, argidx);
 746
 747                 pool<Module*> modules;
 748
 749                 for (auto module : design->modules())
 750                         if (!module->get_blackbox_attribute() && !module->has_memories_warn() && !module->has_processes_warn())
 751                                 modules.insert(module);
 752
 753                 if (template_f.is_open())
 754                 {
 755                         std::string line;
 756                         while (std::getline(template_f, line))
 757                         {
 758                                 int indent = 0;
 759                                 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
 760                                         indent++;
 761
 762                                 if (line[indent] == '%')
 763                                 {
 764                                         vector<string> stmt = split_tokens(line);
 765
 766                                         if (GetSize(stmt) == 1 && stmt[0] == "%%")
 767                                                 break;
 768
 769                                         if (GetSize(stmt) == 2 && stmt[0] == "%module")
 770                                         {
 771                                                 Module *module = design->module(RTLIL::escape_id(stmt[1]));
 772                                                 modules.erase(module);
 773
 774                                                 if (module == nullptr)
 775                                                         log_error("Module '%s' not found.\n", stmt[1].c_str());
 776
 777                                                 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 778
 779                                                 log("Creating SMV representation of module %s.\n", log_id(module));
 780                                                 SmvWorker worker(module, verbose, *f);
 781                                                 worker.run();
 782
 783                                                 *f << stringf("-- end of yosys output\n");
 784                                                 continue;
 785                                         }
 786
 787                                         log_error("Unknown template statement: '%s'", line.c_str() + indent);
 788                                 }
 789
 790                                 *f << line << std::endl;
 791                         }
 792                 }
 793
 794                 if (!modules.empty())
 795                 {
 796                         *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 797
 798                         for (auto module : modules) {
 799                                 log("Creating SMV representation of module %s.\n", log_id(module));
 800                                 SmvWorker worker(module, verbose, *f);
 801                                 worker.run();
 802                         }
 803
 804                         *f << stringf("-- end of yosys output\n");
 805                 }
 806
 807                 if (template_f.is_open()) {
 808                         std::string line;
 809                         while (std::getline(template_f, line))
 810                                 *f << line << std::endl;
 811                 }
 812         }
 813 } SmvBackend;
 814
 815 PRIVATE_NAMESPACE_END