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