backends/btor/btor.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 BtorWorker
  31 {
  32         std::ostream &f;
  33         SigMap sigmap;
  34         RTLIL::Module *module;
  35         bool verbose;
  36
  37         int next_nid = 1;
  38         int initstate_nid = -1;
  39
  40         // <width> => <sid>
  41         dict<int, int> sorts_bv;
  42
  43         // (<address-width>, <data-width>) => <sid>
  44         dict<pair<int, int>, int> sorts_mem;
  45
  46         // SigBit => (<nid>, <bitidx>)
  47         dict<SigBit, pair<int, int>> bit_nid;
  48
  49         // <nid> => <bvwidth>
  50         dict<int, int> nid_width;
  51
  52         // SigSpec => <nid>
  53         dict<SigSpec, int> sig_nid;
  54
  55         // bit to driving cell
  56         dict<SigBit, Cell*> bit_cell;
  57
  58         // nids for constants
  59         dict<Const, int> consts;
  60
  61         // ff inputs that need to be evaluated (<nid>, <ff_cell>)
  62         vector<pair<int, Cell*>> ff_todo;
  63
  64         pool<Cell*> cell_recursion_guard;
  65         pool<string> output_symbols;
  66         string indent;
  67
  68         void btorf(const char *fmt, ...)
  69         {
  70                 va_list ap;
  71                 va_start(ap, fmt);
  72                 f << indent << vstringf(fmt, ap);
  73                 va_end(ap);
  74         }
  75
  76         void btorf_push(const string &id)
  77         {
  78                 if (verbose) {
  79                         f << indent << stringf("  ; begin %s\n", id.c_str());
  80                         indent += "    ";
  81                 }
  82         }
  83
  84         void btorf_pop(const string &id)
  85         {
  86                 if (verbose) {
  87                         indent = indent.substr(4);
  88                         f << indent << stringf("  ; end %s\n", id.c_str());
  89                 }
  90         }
  91
  92         int get_bv_sid(int width)
  93         {
  94                 if (sorts_bv.count(width) == 0) {
  95                         int nid = next_nid++;
  96                         btorf("%d sort bitvec %d\n", nid, width);
  97                         sorts_bv[width] = nid;
  98                 }
  99                 return sorts_bv.at(width);
 100         }
 101
 102         void add_nid_sig(int nid, const SigSpec &sig)
 103         {
 104                 for (int i = 0; i < GetSize(sig); i++)
 105                         bit_nid[sig[i]] = make_pair(nid, i);
 106
 107                 sig_nid[sig] = nid;
 108                 nid_width[nid] = GetSize(sig);
 109         }
 110
 111         void export_cell(Cell *cell)
 112         {
 113                 log_assert(cell_recursion_guard.count(cell) == 0);
 114                 cell_recursion_guard.insert(cell);
 115                 btorf_push(log_id(cell));
 116
 117                 if (cell->type.in("$add", "$sub", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
 118                                 "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
 119                 {
 120                         string btor_op;
 121                         if (cell->type == "$add") btor_op = "add";
 122                         if (cell->type == "$sub") btor_op = "sub";
 123                         if (cell->type.in("$shl", "$sshl")) btor_op = "sll";
 124                         if (cell->type == "$shr") btor_op = "srl";
 125                         if (cell->type == "$sshr") btor_op = "sra";
 126                         if (cell->type.in("$shift", "$shiftx")) btor_op = "shift";
 127                         if (cell->type.in("$and", "$_AND_")) btor_op = "and";
 128                         if (cell->type.in("$or", "$_OR_")) btor_op = "or";
 129                         if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor";
 130                         if (cell->type == "$_NAND_") btor_op = "nand";
 131                         if (cell->type == "$_NOR_") btor_op = "nor";
 132                         if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor";
 133                         log_assert(!btor_op.empty());
 134
 135                         int width = GetSize(cell->getPort("\\Y"));
 136                         width = std::max(width, GetSize(cell->getPort("\\A")));
 137                         width = std::max(width, GetSize(cell->getPort("\\B")));
 138
 139                         bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
 140                         bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
 141
 142                         if (btor_op == "shift" && !b_signed)
 143                                 btor_op = "srl";
 144
 145                         if (cell->type.in("$shl", "$sshl", "$shr", "$sshr"))
 146                                 b_signed = false;
 147
 148                         if (cell->type == "$sshr" && !a_signed)
 149                                 btor_op = "srl";
 150
 151                         int sid = get_bv_sid(width);
 152                         int nid;
 153
 154                         if (btor_op == "shift")
 155                         {
 156                                 int nid_a = get_sig_nid(cell->getPort("\\A"), width, false);
 157                                 int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
 158
 159                                 int nid_r = next_nid++;
 160                                 btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
 161
 162                                 int nid_b_neg = next_nid++;
 163                                 btorf("%d neg %d %d\n", nid_b_neg, sid, nid_b);
 164
 165                                 int nid_l = next_nid++;
 166                                 btorf("%d sll %d %d %d\n", nid_l, sid, nid_a, nid_b_neg);
 167
 168                                 int sid_bit = get_bv_sid(1);
 169                                 int nid_zero = get_sig_nid(Const(0, width));
 170                                 int nid_b_ltz = next_nid++;
 171                                 btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero);
 172
 173                                 nid = next_nid++;
 174                                 btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r);
 175                         }
 176                         else
 177                         {
 178                                 int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
 179                                 int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
 180
 181                                 nid = next_nid++;
 182                                 btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
 183                         }
 184
 185                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 186
 187                         if (GetSize(sig) < width) {
 188                                 int sid = get_bv_sid(GetSize(sig));
 189                                 int nid2 = next_nid++;
 190                                 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
 191                                 nid = nid2;
 192                         }
 193
 194                         add_nid_sig(nid, sig);
 195                         goto okay;
 196                 }
 197
 198                 if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
 199                 {
 200                         int sid = get_bv_sid(1);
 201                         int nid_a = get_sig_nid(cell->getPort("\\A"));
 202                         int nid_b = get_sig_nid(cell->getPort("\\B"));
 203
 204                         int nid1 = next_nid++;
 205                         int nid2 = next_nid++;
 206
 207                         if (cell->type == "$_ANDNOT_") {
 208                                 btorf("%d not %d %d\n", nid1, sid, nid_b);
 209                                 btorf("%d and %d %d %d\n", nid2, sid, nid_a, nid1);
 210                         }
 211
 212                         if (cell->type == "$_ORNOT_") {
 213                                 btorf("%d not %d %d\n", nid1, sid, nid_b);
 214                                 btorf("%d or %d %d %d\n", nid2, sid, nid_a, nid1);
 215                         }
 216
 217                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 218                         add_nid_sig(nid2, sig);
 219                         goto okay;
 220                 }
 221
 222                 if (cell->type.in("$_OAI3_", "$_AOI3_"))
 223                 {
 224                         int sid = get_bv_sid(1);
 225                         int nid_a = get_sig_nid(cell->getPort("\\A"));
 226                         int nid_b = get_sig_nid(cell->getPort("\\B"));
 227                         int nid_c = get_sig_nid(cell->getPort("\\C"));
 228
 229                         int nid1 = next_nid++;
 230                         int nid2 = next_nid++;
 231                         int nid3 = next_nid++;
 232
 233                         if (cell->type == "$_OAI3_") {
 234                                 btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
 235                                 btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c);
 236                                 btorf("%d not %d %d\n", nid3, sid, nid2);
 237                         }
 238
 239                         if (cell->type == "$_AOI3_") {
 240                                 btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
 241                                 btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c);
 242                                 btorf("%d not %d %d\n", nid3, sid, nid2);
 243                         }
 244
 245                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 246                         add_nid_sig(nid3, sig);
 247                         goto okay;
 248                 }
 249
 250                 if (cell->type.in("$_OAI4_", "$_AOI4_"))
 251                 {
 252                         int sid = get_bv_sid(1);
 253                         int nid_a = get_sig_nid(cell->getPort("\\A"));
 254                         int nid_b = get_sig_nid(cell->getPort("\\B"));
 255                         int nid_c = get_sig_nid(cell->getPort("\\C"));
 256                         int nid_d = get_sig_nid(cell->getPort("\\D"));
 257
 258                         int nid1 = next_nid++;
 259                         int nid2 = next_nid++;
 260                         int nid3 = next_nid++;
 261                         int nid4 = next_nid++;
 262
 263                         if (cell->type == "$_OAI4_") {
 264                                 btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
 265                                 btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d);
 266                                 btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2);
 267                                 btorf("%d not %d %d\n", nid4, sid, nid3);
 268                         }
 269
 270                         if (cell->type == "$_AOI4_") {
 271                                 btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
 272                                 btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d);
 273                                 btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2);
 274                                 btorf("%d not %d %d\n", nid4, sid, nid3);
 275                         }
 276
 277                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 278                         add_nid_sig(nid4, sig);
 279                         goto okay;
 280                 }
 281
 282                 if (cell->type.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
 283                 {
 284                         string btor_op;
 285                         if (cell->type == "$lt") btor_op = "lt";
 286                         if (cell->type == "$le") btor_op = "lte";
 287                         if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
 288                         if (cell->type.in("$ne", "$nex")) btor_op = "ne";
 289                         if (cell->type == "$ge") btor_op = "gte";
 290                         if (cell->type == "$gt") btor_op = "gt";
 291                         log_assert(!btor_op.empty());
 292
 293                         int width = 1;
 294                         width = std::max(width, GetSize(cell->getPort("\\A")));
 295                         width = std::max(width, GetSize(cell->getPort("\\B")));
 296
 297                         bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
 298                         bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
 299
 300                         int sid = get_bv_sid(1);
 301                         int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
 302                         int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
 303
 304                         int nid = next_nid++;
 305                         if (cell->type.in("$lt", "$le", "$ge", "$gt")) {
 306                                 btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
 307                         } else {
 308                                 btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
 309                         }
 310
 311                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 312
 313                         if (GetSize(sig) > 1) {
 314                                 int sid = get_bv_sid(GetSize(sig));
 315                                 int nid2 = next_nid++;
 316                                 btorf("%d uext %d %d %d\n", nid2, sid, nid, GetSize(sig) - 1);
 317                                 nid = nid2;
 318                         }
 319
 320                         add_nid_sig(nid, sig);
 321                         goto okay;
 322                 }
 323
 324                 if (cell->type.in("$not", "$neg", "$_NOT_"))
 325                 {
 326                         string btor_op;
 327                         if (cell->type.in("$not", "$_NOT_")) btor_op = "not";
 328                         if (cell->type == "$neg") btor_op = "neg";
 329                         log_assert(!btor_op.empty());
 330
 331                         int width = GetSize(cell->getPort("\\Y"));
 332                         width = std::max(width, GetSize(cell->getPort("\\A")));
 333
 334                         bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
 335
 336                         int sid = get_bv_sid(width);
 337                         int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
 338
 339                         int nid = next_nid++;
 340                         btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
 341
 342                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 343
 344                         if (GetSize(sig) < width) {
 345                                 int sid = get_bv_sid(GetSize(sig));
 346                                 int nid2 = next_nid++;
 347                                 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
 348                                 nid = nid2;
 349                         }
 350
 351                         add_nid_sig(nid, sig);
 352                         goto okay;
 353                 }
 354
 355                 if (cell->type.in("$logic_and", "$logic_or", "$logic_not"))
 356                 {
 357                         string btor_op;
 358                         if (cell->type == "$logic_and") btor_op = "and";
 359                         if (cell->type == "$logic_or")  btor_op = "or";
 360                         if (cell->type == "$logic_not") btor_op = "not";
 361                         log_assert(!btor_op.empty());
 362
 363                         int sid = get_bv_sid(1);
 364                         int nid_a = get_sig_nid(cell->getPort("\\A"));
 365                         int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort("\\B")) : 0;
 366
 367                         if (GetSize(cell->getPort("\\A")) > 1) {
 368                                 int nid_red_a = next_nid++;
 369                                 btorf("%d redor %d %d\n", nid_red_a, sid, nid_a);
 370                                 nid_a = nid_red_a;
 371                         }
 372
 373                         if (btor_op != "not" && GetSize(cell->getPort("\\B")) > 1) {
 374                                 int nid_red_b = next_nid++;
 375                                 btorf("%d redor %d %d\n", nid_red_b, sid, nid_b);
 376                                 nid_b = nid_red_b;
 377                         }
 378
 379                         int nid = next_nid++;
 380                         if (btor_op != "not")
 381                                 btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
 382                         else
 383                                 btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
 384
 385                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 386
 387                         if (GetSize(sig) > 1) {
 388                                 int sid = get_bv_sid(GetSize(sig));
 389                                 int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1));
 390                                 int nid2 = next_nid++;
 391                                 btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid);
 392                                 nid = nid2;
 393                         }
 394
 395                         add_nid_sig(nid, sig);
 396                         goto okay;
 397                 }
 398
 399                 if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
 400                 {
 401                         string btor_op;
 402                         if (cell->type == "$reduce_and") btor_op = "redand";
 403                         if (cell->type.in("$reduce_or", "$reduce_bool")) btor_op = "redor";
 404                         if (cell->type.in("$reduce_xor", "$reduce_xnor")) btor_op = "redxor";
 405                         log_assert(!btor_op.empty());
 406
 407                         int sid = get_bv_sid(1);
 408                         int nid_a = get_sig_nid(cell->getPort("\\A"));
 409
 410                         int nid = next_nid++;
 411                         btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
 412
 413                         if (cell->type == "$reduce_xnor") {
 414                                 int nid2 = next_nid++;
 415                                 btorf("%d not %d %d %d\n", nid2, sid, nid);
 416                                 nid = nid2;
 417                         }
 418
 419                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 420
 421                         if (GetSize(sig) > 1) {
 422                                 int sid = get_bv_sid(GetSize(sig));
 423                                 int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1));
 424                                 int nid2 = next_nid++;
 425                                 btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid);
 426                                 nid = nid2;
 427                         }
 428
 429                         add_nid_sig(nid, sig);
 430                         goto okay;
 431                 }
 432
 433                 if (cell->type.in("$mux", "$_MUX_"))
 434                 {
 435                         SigSpec sig_a = sigmap(cell->getPort("\\A"));
 436                         SigSpec sig_b = sigmap(cell->getPort("\\B"));
 437                         SigSpec sig_s = sigmap(cell->getPort("\\S"));
 438                         SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 439
 440                         int nid_a = get_sig_nid(sig_a);
 441                         int nid_b = get_sig_nid(sig_b);
 442                         int nid_s = get_sig_nid(sig_s);
 443
 444                         int sid = get_bv_sid(GetSize(sig_y));
 445                         int nid = next_nid++;
 446                         btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
 447
 448                         add_nid_sig(nid, sig_y);
 449                         goto okay;
 450                 }
 451
 452                 if (cell->type == "$pmux")
 453                 {
 454                         SigSpec sig_a = sigmap(cell->getPort("\\A"));
 455                         SigSpec sig_b = sigmap(cell->getPort("\\B"));
 456                         SigSpec sig_s = sigmap(cell->getPort("\\S"));
 457                         SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 458
 459                         int width = GetSize(sig_a);
 460                         int sid = get_bv_sid(width);
 461                         int nid = get_sig_nid(sig_a);
 462
 463                         for (int i = 0; i < GetSize(sig_s); i++) {
 464                                 int nid_b = get_sig_nid(sig_b.extract(i*width, width));
 465                                 int nid_s = get_sig_nid(sig_s.extract(i));
 466                                 int nid2 = next_nid++;
 467                                 btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
 468                                 nid = nid2;
 469                         }
 470
 471                         add_nid_sig(nid, sig_y);
 472                         goto okay;
 473                 }
 474
 475                 if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
 476                 {
 477                         SigSpec sig_d = sigmap(cell->getPort("\\D"));
 478                         SigSpec sig_q = sigmap(cell->getPort("\\Q"));
 479
 480                         string symbol = log_signal(sig_q);
 481                         if (symbol.find(' ') != string::npos)
 482                                 symbol = log_id(cell);
 483
 484                         if (symbol[0] == '\\')
 485                                 symbol = symbol.substr(1);
 486
 487                         int sid = get_bv_sid(GetSize(sig_q));
 488                         int nid = next_nid++;
 489
 490                         if (output_symbols.count(symbol))
 491                                 btorf("%d state %d\n", nid, sid);
 492                         else
 493                                 btorf("%d state %d %s\n", nid, sid, symbol.c_str());
 494
 495                         ff_todo.push_back(make_pair(nid, cell));
 496                         add_nid_sig(nid, sig_q);
 497                         goto okay;
 498                 }
 499
 500                 if (cell->type == "$initstate")
 501                 {
 502                         SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 503
 504                         if (initstate_nid < 0)
 505                         {
 506                                 int sid = get_bv_sid(1);
 507                                 int one_nid = get_sig_nid(Const(1, 1));
 508                                 int zero_nid = get_sig_nid(Const(0, 1));
 509                                 initstate_nid = next_nid++;
 510                                 btorf("%d state %d\n", initstate_nid, sid);
 511                                 btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
 512                                 btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
 513                         }
 514
 515                         add_nid_sig(initstate_nid, sig_y);
 516                         goto okay;
 517                 }
 518
 519                 log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
 520
 521         okay:
 522                 btorf_pop(log_id(cell));
 523                 cell_recursion_guard.erase(cell);
 524         }
 525
 526         int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
 527         {
 528                 sigmap.apply(sig);
 529
 530                 if (sig_nid.count(sig) == 0)
 531                 {
 532                         // <nid>, <bitidx>
 533                         vector<pair<int, int>> nidbits;
 534
 535                         // collect all bits
 536                         for (int i = 0; i < GetSize(sig); i++)
 537                         {
 538                                 SigBit bit = sig[i];
 539
 540                                 if (bit_nid.count(bit) == 0)
 541                                 {
 542                                         if (bit.wire == nullptr)
 543                                         {
 544                                                 Const c(bit.data);
 545
 546                                                 while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr)
 547                                                         c.bits.push_back(sig[i+GetSize(c)].data);
 548
 549                                                 if (consts.count(c) == 0) {
 550                                                         int sid = get_bv_sid(GetSize(c));
 551                                                         int nid = next_nid++;
 552                                                         btorf("%d const %d %s\n", nid, sid, c.as_string().c_str());
 553                                                         consts[c] = nid;
 554                                                         nid_width[nid] = GetSize(c);
 555                                                 }
 556
 557                                                 int nid = consts.at(c);
 558
 559                                                 for (int j = 0; j < GetSize(c); j++)
 560                                                         nidbits.push_back(make_pair(nid, j));
 561
 562                                                 i += GetSize(c)-1;
 563                                                 continue;
 564                                         }
 565                                         else
 566                                         {
 567                                                 export_cell(bit_cell.at(bit));
 568                                                 log_assert(bit_nid.count(bit));
 569                                         }
 570                                 }
 571
 572                                 nidbits.push_back(bit_nid.at(bit));
 573                         }
 574
 575                         int width = 0;
 576                         int nid = -1;
 577
 578                         // group bits and emit slice-concat chain
 579                         for (int i = 0; i < GetSize(nidbits); i++)
 580                         {
 581                                 int nid2 = nidbits[i].first;
 582                                 int lower =  nidbits[i].second;
 583                                 int upper = lower;
 584
 585                                 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first &&
 586                                                 nidbits[i+1].second == nidbits[i].second+1)
 587                                         upper++, i++;
 588
 589                                 int nid3 = nid2;
 590
 591                                 if (lower != 0 || upper+1 != nid_width.at(nid2)) {
 592                                         int sid = get_bv_sid(upper-lower+1);
 593                                         nid3 = next_nid++;
 594                                         btorf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower);
 595                                 }
 596
 597                                 int nid4 = nid3;
 598
 599                                 if (nid >= 0) {
 600                                         int sid = get_bv_sid(width+upper-lower+1);
 601                                         nid4 = next_nid++;
 602                                         btorf("%d concat %d %d %d\n", nid4, sid, nid3, nid);
 603                                 }
 604
 605                                 width += upper-lower+1;
 606                                 nid = nid4;
 607                         }
 608
 609                         sig_nid[sig] = nid;
 610                         nid_width[nid] = width;
 611                 }
 612
 613                 int nid = sig_nid.at(sig);
 614
 615                 if (to_width >= 0 && to_width != GetSize(sig))
 616                 {
 617                         if (to_width < GetSize(sig))
 618                         {
 619                                 int sid = get_bv_sid(to_width);
 620                                 int nid2 = next_nid++;
 621                                 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1);
 622                                 nid = nid2;
 623                         }
 624                         else
 625                         {
 626                                 int sid = get_bv_sid(to_width);
 627                                 int nid2 = next_nid++;
 628                                 btorf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext",
 629                                                 sid, nid, to_width - GetSize(sig));
 630                                 nid = nid2;
 631                         }
 632                 }
 633
 634                 return nid;
 635         }
 636
 637         BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
 638                         f(f), sigmap(module), module(module), verbose(verbose)
 639         {
 640                 btorf_push("inputs");
 641
 642                 for (auto wire : module->wires())
 643                 {
 644                         if (!wire->port_id || !wire->port_input)
 645                                 continue;
 646
 647                         SigSpec sig = sigmap(wire);
 648                         int sid = get_bv_sid(GetSize(sig));
 649                         int nid = next_nid++;
 650
 651                         btorf("%d input %d %s\n", nid, sid, log_id(wire));
 652                         add_nid_sig(nid, sig);
 653                 }
 654
 655                 btorf_pop("inputs");
 656
 657                 for (auto cell : module->cells())
 658                 for (auto &conn : cell->connections())
 659                 {
 660                         if (!cell->output(conn.first))
 661                                 continue;
 662
 663                         for (auto bit : sigmap(conn.second))
 664                                 bit_cell[bit] = cell;
 665                 }
 666
 667                 for (auto wire : module->wires())
 668                         if (wire->port_output)
 669                                 output_symbols.insert(log_id(wire));
 670
 671                 for (auto wire : module->wires())
 672                 {
 673                         if (!wire->port_id || !wire->port_output)
 674                                 continue;
 675
 676                         btorf_push(stringf("output %s", log_id(wire)));
 677
 678                         int sid = get_bv_sid(GetSize(wire));
 679                         int nid = get_sig_nid(wire);
 680                         btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
 681
 682                         btorf_pop(stringf("output %s", log_id(wire)));
 683                 }
 684
 685                 for (auto cell : module->cells())
 686                 {
 687                         if (cell->type == "$assume")
 688                         {
 689                                 btorf_push(log_id(cell));
 690
 691                                 int sid = get_bv_sid(1);
 692                                 int nid_a = get_sig_nid(cell->getPort("\\A"));
 693                                 int nid_en = get_sig_nid(cell->getPort("\\EN"));
 694                                 int nid_not_en = next_nid++;
 695                                 int nid_a_or_not_en = next_nid++;
 696                                 int nid = next_nid++;
 697
 698                                 btorf("%d not %d %d\n", nid_not_en, sid, nid_en);
 699                                 btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en);
 700                                 btorf("%d constraint %d\n", nid, nid_a_or_not_en);
 701
 702                                 btorf_pop(log_id(cell));
 703                         }
 704
 705                         if (cell->type == "$assert")
 706                         {
 707                                 btorf_push(log_id(cell));
 708
 709                                 int sid = get_bv_sid(1);
 710                                 int nid_a = get_sig_nid(cell->getPort("\\A"));
 711                                 int nid_en = get_sig_nid(cell->getPort("\\EN"));
 712                                 int nid_not_a = next_nid++;
 713                                 int nid_en_and_not_a = next_nid++;
 714                                 int nid = next_nid++;
 715
 716                                 btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
 717                                 btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
 718                                 btorf("%d bad %d\n", nid, nid_en_and_not_a);
 719
 720                                 btorf_pop(log_id(cell));
 721                         }
 722                 }
 723
 724                 while (!ff_todo.empty())
 725                 {
 726                         vector<pair<int, Cell*>> todo;
 727                         todo.swap(ff_todo);
 728
 729                         for (auto &it : todo)
 730                         {
 731                                 btorf_push(stringf("next %s", log_id(it.second)));
 732
 733                                 SigSpec sig = sigmap(it.second->getPort("\\D"));
 734
 735                                 int nid = get_sig_nid(sig);
 736                                 int sid = get_bv_sid(GetSize(sig));
 737                                 btorf("%d next %d %d %d\n", next_nid++, sid, it.first, nid);
 738
 739                                 btorf_pop(stringf("next %s", log_id(it.second)));
 740                         }
 741                 }
 742         }
 743 };
 744
 745 struct BtorBackend : public Backend {
 746         BtorBackend() : Backend("btor", "write design to BTOR file") { }
 747         virtual void help()
 748         {
 749                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 750                 log("\n");
 751                 log("    write_btor [options] [filename]\n");
 752                 log("\n");
 753                 log("Write a BTOR description of the current design.\n");
 754                 log("\n");
 755                 log("  -v\n");
 756                 log("    Add comments and indentation to BTOR output file\n");
 757                 log("\n");
 758         }
 759         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 760         {
 761                 bool verbose = false;
 762
 763                 log_header(design, "Executing BTOR backend.\n");
 764
 765                 size_t argidx;
 766                 for (argidx = 1; argidx < args.size(); argidx++)
 767                 {
 768                         if (args[argidx] == "-v") {
 769                                 verbose = true;
 770                                 continue;
 771                         }
 772                         break;
 773                 }
 774                 extra_args(f, filename, args, argidx);
 775
 776                 RTLIL::Module *topmod = design->top_module();
 777
 778                 if (topmod == nullptr)
 779                         log_cmd_error("No top module found.\n");
 780
 781                 *f << stringf("; BTOR description generated by %s for module %s.\n",
 782                                 yosys_version_str, log_id(topmod));
 783
 784                 BtorWorker(*f, topmod, verbose);
 785
 786                 *f << stringf("; end of yosys output\n");
 787         }
 788 } BtorBackend;
 789
 790 PRIVATE_NAMESPACE_END