backends/smv/smv.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
   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                                 if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) {
 578                                         log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n",
 579                                                         log_id(cell->type), log_id(module), log_id(cell));
 580                                 }
 581                                 if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") {
 582                                         log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smv`.\n",
 583                                                         log_id(cell->type), log_id(module), log_id(cell));
 584                                 }
 585                                 if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") {
 586                                         log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smv`.\n",
 587                                                         log_id(cell->type), log_id(module), log_id(cell));
 588                                 }
 589                                 log_error("Unsupported cell type %s for cell %s.%s.\n",
 590                                                 log_id(cell->type), log_id(module), log_id(cell));
 591                         }
 592
 593 //                      f << stringf("    %s : %s;\n", cid(cell->name), cid(cell->type));
 594
 595                         for (auto &conn : cell->connections())
 596                                 if (cell->output(conn.first))
 597                                         definitions.push_back(stringf("%s := %s.%s;", lvalue(conn.second), cid(cell->name), cid(conn.first)));
 598                                 else
 599                                         definitions.push_back(stringf("%s.%s := %s;", cid(cell->name), cid(conn.first), rvalue(conn.second)));
 600                 }
 601
 602                 for (Wire *wire : partial_assignment_wires)
 603                 {
 604                         string expr;
 605
 606                         for (int i = 0; i < wire->width; i++)
 607                         {
 608                                 if (!expr.empty())
 609                                         expr = " :: " + expr;
 610
 611                                 if (partial_assignment_bits.count(sigmap(SigBit(wire, i))))
 612                                 {
 613                                         int width = 1;
 614                                         const auto &bit_a = partial_assignment_bits.at(sigmap(SigBit(wire, i)));
 615
 616                                         while (i+1 < wire->width)
 617                                         {
 618                                                 SigBit next_bit = sigmap(SigBit(wire, i+1));
 619
 620                                                 if (!partial_assignment_bits.count(next_bit))
 621                                                         break;
 622
 623                                                 const auto &bit_b = partial_assignment_bits.at(next_bit);
 624                                                 if (strcmp(bit_a.first, bit_b.first))
 625                                                         break;
 626                                                 if (bit_a.second+width != bit_b.second)
 627                                                         break;
 628
 629                                                 width++, i++;
 630                                         }
 631
 632                                         expr = stringf("%s[%d:%d]", bit_a.first, bit_a.second+width-1, bit_a.second) + expr;
 633                                 }
 634                                 else if (sigmap(SigBit(wire, i)).wire == nullptr)
 635                                 {
 636                                         string bits;
 637                                         SigSpec sig = sigmap(SigSpec(wire, i));
 638
 639                                         while (i+1 < wire->width) {
 640                                                 SigBit next_bit = sigmap(SigBit(wire, i+1));
 641                                                 if (next_bit.wire != nullptr)
 642                                                         break;
 643                                                 sig.append(next_bit);
 644                                                 i++;
 645                                         }
 646
 647                                         for (int k = GetSize(sig)-1; k >= 0; k--)
 648                                                 bits += sig[k] == State::S1 ? '1' : '0';
 649
 650                                         expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr;
 651                                 }
 652                                 else if (sigmap(SigBit(wire, i)) == SigBit(wire, i))
 653                                 {
 654                                         int length = 1;
 655
 656                                         while (i+1 < wire->width) {
 657                                                 if (partial_assignment_bits.count(sigmap(SigBit(wire, i+1))))
 658                                                         break;
 659                                                 if (sigmap(SigBit(wire, i+1)) != SigBit(wire, i+1))
 660                                                         break;
 661                                                 i++, length++;
 662                                         }
 663
 664                                         expr = stringf("0ub%d_0", length) + expr;
 665                                 }
 666                                 else
 667                                 {
 668                                         string bits;
 669                                         SigSpec sig = sigmap(SigSpec(wire, i));
 670
 671                                         while (i+1 < wire->width) {
 672                                                 SigBit next_bit = sigmap(SigBit(wire, i+1));
 673                                                 if (next_bit.wire == nullptr || partial_assignment_bits.count(next_bit))
 674                                                         break;
 675                                                 sig.append(next_bit);
 676                                                 i++;
 677                                         }
 678
 679                                         expr = rvalue(sig) + expr;
 680                                 }
 681                         }
 682
 683                         definitions.push_back(stringf("%s := %s;", cid(wire->name), expr.c_str()));
 684                 }
 685
 686                 if (!inputvars.empty()) {
 687                         f << stringf("  IVAR\n");
 688                         for (const string &line : inputvars)
 689                                 f << stringf("    %s\n", line.c_str());
 690                 }
 691
 692                 if (!vars.empty()) {
 693                         f << stringf("  VAR\n");
 694                         for (const string &line : vars)
 695                                 f << stringf("    %s\n", line.c_str());
 696                 }
 697
 698                 if (!definitions.empty()) {
 699                         f << stringf("  DEFINE\n");
 700                         for (const string &line : definitions)
 701                                 f << stringf("    %s\n", line.c_str());
 702                 }
 703
 704                 if (!assignments.empty()) {
 705                         f << stringf("  ASSIGN\n");
 706                         for (const string &line : assignments)
 707                                 f << stringf("    %s\n", line.c_str());
 708                 }
 709
 710                 if (!invarspecs.empty()) {
 711                         for (const string &line : invarspecs)
 712                                 f << stringf("  INVARSPEC %s\n", line.c_str());
 713                 }
 714         }
 715 };
 716
 717 struct SmvBackend : public Backend {
 718         SmvBackend() : Backend("smv", "write design to SMV file") { }
 719         void help() override
 720         {
 721                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 722                 log("\n");
 723                 log("    write_smv [options] [filename]\n");
 724                 log("\n");
 725                 log("Write an SMV description of the current design.\n");
 726                 log("\n");
 727                 log("    -verbose\n");
 728                 log("        this will print the recursive walk used to export the modules.\n");
 729                 log("\n");
 730                 log("    -tpl <template_file>\n");
 731                 log("        use the given template file. the line containing only the token '%%%%'\n");
 732                 log("        is replaced with the regular output of this command.\n");
 733                 log("\n");
 734                 log("THIS COMMAND IS UNDER CONSTRUCTION\n");
 735                 log("\n");
 736         }
 737         void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
 738         {
 739                 std::ifstream template_f;
 740                 bool verbose = false;
 741
 742                 log_header(design, "Executing SMV backend.\n");
 743
 744                 log_push();
 745                 Pass::call(design, "bmuxmap");
 746                 Pass::call(design, "demuxmap");
 747                 log_pop();
 748
 749                 size_t argidx;
 750                 for (argidx = 1; argidx < args.size(); argidx++)
 751                 {
 752                         if (args[argidx] == "-tpl" && argidx+1 < args.size()) {
 753                                 template_f.open(args[++argidx]);
 754                                 if (template_f.fail())
 755                                         log_error("Can't open template file `%s'.\n", args[argidx].c_str());
 756                                 continue;
 757                         }
 758                         if (args[argidx] == "-verbose") {
 759                                 verbose = true;
 760                                 continue;
 761                         }
 762                         break;
 763                 }
 764                 extra_args(f, filename, args, argidx);
 765
 766                 pool<Module*> modules;
 767
 768                 for (auto module : design->modules())
 769                         if (!module->get_blackbox_attribute() && !module->has_memories_warn() && !module->has_processes_warn())
 770                                 modules.insert(module);
 771
 772                 if (template_f.is_open())
 773                 {
 774                         std::string line;
 775                         while (std::getline(template_f, line))
 776                         {
 777                                 int indent = 0;
 778                                 while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t'))
 779                                         indent++;
 780
 781                                 if (line[indent] == '%')
 782                                 {
 783                                         vector<string> stmt = split_tokens(line);
 784
 785                                         if (GetSize(stmt) == 1 && stmt[0] == "%%")
 786                                                 break;
 787
 788                                         if (GetSize(stmt) == 2 && stmt[0] == "%module")
 789                                         {
 790                                                 Module *module = design->module(RTLIL::escape_id(stmt[1]));
 791                                                 modules.erase(module);
 792
 793                                                 if (module == nullptr)
 794                                                         log_error("Module '%s' not found.\n", stmt[1].c_str());
 795
 796                                                 *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 797
 798                                                 log("Creating SMV representation of module %s.\n", log_id(module));
 799                                                 SmvWorker worker(module, verbose, *f);
 800                                                 worker.run();
 801
 802                                                 *f << stringf("-- end of yosys output\n");
 803                                                 continue;
 804                                         }
 805
 806                                         log_error("Unknown template statement: '%s'", line.c_str() + indent);
 807                                 }
 808
 809                                 *f << line << std::endl;
 810                         }
 811                 }
 812
 813                 if (!modules.empty())
 814                 {
 815                         *f << stringf("-- SMV description generated by %s\n", yosys_version_str);
 816
 817                         for (auto module : modules) {
 818                                 log("Creating SMV representation of module %s.\n", log_id(module));
 819                                 SmvWorker worker(module, verbose, *f);
 820                                 worker.run();
 821                         }
 822
 823                         *f << stringf("-- end of yosys output\n");
 824                 }
 825
 826                 if (template_f.is_open()) {
 827                         std::string line;
 828                         while (std::getline(template_f, line))
 829                                 *f << line << std::endl;
 830                 }
 831         }
 832 } SmvBackend;
 833
 834 PRIVATE_NAMESPACE_END