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", "$xor"))
 118                 {
 119                         string btor_op;
 120                         if (cell->type == "$add") btor_op = "add";
 121                         if (cell->type == "$sub") btor_op = "sub";
 122                         if (cell->type == "$xor") btor_op = "xor";
 123                         log_assert(!btor_op.empty());
 124
 125                         int width = GetSize(cell->getPort("\\Y"));
 126                         width = std::max(width, GetSize(cell->getPort("\\A")));
 127                         width = std::max(width, GetSize(cell->getPort("\\B")));
 128
 129                         bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
 130                         bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
 131
 132                         int sid = get_bv_sid(width);
 133                         int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
 134                         int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
 135
 136                         int nid = next_nid++;
 137                         btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
 138
 139                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 140
 141                         if (GetSize(sig) < width) {
 142                                 int sid = get_bv_sid(GetSize(sig));
 143                                 int nid2 = next_nid++;
 144                                 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
 145                                 nid = nid2;
 146                         }
 147
 148                         add_nid_sig(nid, sig);
 149                         goto okay;
 150                 }
 151
 152                 if (cell->type.in("$logic_and", "$logic_or"))
 153                 {
 154                         string btor_op;
 155                         if (cell->type == "$logic_and") btor_op = "and";
 156                         if (cell->type == "$logic_or")  btor_op = "or";
 157                         log_assert(!btor_op.empty());
 158
 159                         int sid = get_bv_sid(1);
 160                         int nid_a = get_sig_nid(cell->getPort("\\A"));
 161                         int nid_b = get_sig_nid(cell->getPort("\\B"));
 162
 163                         if (GetSize(cell->getPort("\\A")) > 1) {
 164                                 int nid_red_a = next_nid++;
 165                                 btorf("%d redor %d %d\n", nid_red_a, sid, nid_a);
 166                                 nid_a = nid_red_a;
 167                         }
 168
 169                         if (GetSize(cell->getPort("\\B")) > 1) {
 170                                 int nid_red_b = next_nid++;
 171                                 btorf("%d redor %d %d\n", nid_red_b, sid, nid_b);
 172                                 nid_b = nid_red_b;
 173                         }
 174
 175                         int nid = next_nid++;
 176                         btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
 177
 178                         SigSpec sig = sigmap(cell->getPort("\\Y"));
 179
 180                         if (GetSize(sig) > 1) {
 181                                 int sid = get_bv_sid(GetSize(sig));
 182                                 int zeros_nid = get_sig_nid(Const(0, GetSize(sig)-1));
 183                                 int nid2 = next_nid++;
 184                                 btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid);
 185                                 nid = nid2;
 186                         }
 187
 188                         add_nid_sig(nid, sig);
 189                         goto okay;
 190                 }
 191
 192                 if (cell->type.in("$mux", "$_MUX_"))
 193                 {
 194                         SigSpec sig_a = sigmap(cell->getPort("\\A"));
 195                         SigSpec sig_b = sigmap(cell->getPort("\\B"));
 196                         SigSpec sig_s = sigmap(cell->getPort("\\S"));
 197                         SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 198
 199                         int nid_a = get_sig_nid(sig_a);
 200                         int nid_b = get_sig_nid(sig_b);
 201                         int nid_s = get_sig_nid(sig_s);
 202
 203                         int sid = get_bv_sid(GetSize(sig_y));
 204                         int nid = next_nid++;
 205                         btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
 206
 207                         add_nid_sig(nid, sig_y);
 208                         goto okay;
 209                 }
 210
 211                 if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
 212                 {
 213                         SigSpec sig_d = sigmap(cell->getPort("\\D"));
 214                         SigSpec sig_q = sigmap(cell->getPort("\\Q"));
 215
 216                         string symbol = log_signal(sig_q);
 217                         if (symbol.find(' ') != string::npos)
 218                                 symbol = log_id(cell);
 219
 220                         if (symbol[0] == '\\')
 221                                 symbol = symbol.substr(1);
 222
 223                         int sid = get_bv_sid(GetSize(sig_q));
 224                         int nid = next_nid++;
 225
 226                         if (output_symbols.count(symbol))
 227                                 btorf("%d state %d\n", nid, sid);
 228                         else
 229                                 btorf("%d state %d %s\n", nid, sid, symbol.c_str());
 230
 231                         ff_todo.push_back(make_pair(nid, cell));
 232                         add_nid_sig(nid, sig_q);
 233                         goto okay;
 234                 }
 235
 236                 if (cell->type == "$initstate")
 237                 {
 238                         SigSpec sig_y = sigmap(cell->getPort("\\Y"));
 239
 240                         if (initstate_nid < 0)
 241                         {
 242                                 int sid = get_bv_sid(1);
 243                                 int one_nid = get_sig_nid(Const(1, 1));
 244                                 int zero_nid = get_sig_nid(Const(0, 1));
 245                                 initstate_nid = next_nid++;
 246                                 btorf("%d state %d\n", initstate_nid, sid);
 247                                 btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
 248                                 btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
 249                         }
 250
 251                         add_nid_sig(initstate_nid, sig_y);
 252                         goto okay;
 253                 }
 254
 255                 log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
 256
 257         okay:
 258                 btorf_pop(log_id(cell));
 259                 cell_recursion_guard.erase(cell);
 260         }
 261
 262         int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
 263         {
 264                 sigmap.apply(sig);
 265
 266                 if (sig_nid.count(sig) == 0)
 267                 {
 268                         // <nid>, <bitidx>
 269                         vector<pair<int, int>> nidbits;
 270
 271                         // collect all bits
 272                         for (int i = 0; i < GetSize(sig); i++)
 273                         {
 274                                 SigBit bit = sig[i];
 275
 276                                 if (bit_nid.count(bit) == 0)
 277                                 {
 278                                         if (bit.wire == nullptr)
 279                                         {
 280                                                 Const c(bit.data);
 281
 282                                                 while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr)
 283                                                         c.bits.push_back(sig[i+GetSize(c)].data);
 284
 285                                                 if (consts.count(c) == 0) {
 286                                                         int sid = get_bv_sid(GetSize(c));
 287                                                         int nid = next_nid++;
 288                                                         btorf("%d const %d %s\n", nid, sid, c.as_string().c_str());
 289                                                         consts[c] = nid;
 290                                                         nid_width[nid] = GetSize(c);
 291                                                 }
 292
 293                                                 int nid = consts.at(c);
 294
 295                                                 for (int j = 0; j < GetSize(c); j++)
 296                                                         nidbits.push_back(make_pair(nid, j));
 297
 298                                                 i += GetSize(c)-1;
 299                                                 continue;
 300                                         }
 301                                         else
 302                                         {
 303                                                 export_cell(bit_cell.at(bit));
 304                                                 log_assert(bit_nid.count(bit));
 305                                         }
 306                                 }
 307
 308                                 nidbits.push_back(bit_nid.at(bit));
 309                         }
 310
 311                         int width = 0;
 312                         int nid = -1;
 313
 314                         // group bits and emit slice-concat chain
 315                         for (int i = 0; i < GetSize(nidbits); i++)
 316                         {
 317                                 int nid2 = nidbits[i].first;
 318                                 int lower =  nidbits[i].second;
 319                                 int upper = lower;
 320
 321                                 while (i+1 < GetSize(nidbits) && nidbits[i+1].first == nidbits[i].first &&
 322                                                 nidbits[i+1].second == nidbits[i].second+1)
 323                                         upper++, i++;
 324
 325                                 int nid3 = nid2;
 326
 327                                 if (lower != 0 || upper+1 != nid_width.at(nid2)) {
 328                                         int sid = get_bv_sid(upper-lower+1);
 329                                         nid3 = next_nid++;
 330                                         btorf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower);
 331                                 }
 332
 333                                 int nid4 = nid3;
 334
 335                                 if (nid >= 0) {
 336                                         int sid = get_bv_sid(width+upper-lower+1);
 337                                         nid4 = next_nid++;
 338                                         btorf("%d concat %d %d %d\n", nid4, sid, nid, nid3);
 339                                 }
 340
 341                                 width += upper-lower+1;
 342                                 nid = nid4;
 343                         }
 344
 345                         sig_nid[sig] = nid;
 346                         nid_width[nid] = width;
 347                 }
 348
 349                 int nid = sig_nid.at(sig);
 350
 351                 if (to_width >= 0 && to_width != GetSize(sig))
 352                 {
 353                         if (to_width < GetSize(sig))
 354                         {
 355                                 int sid = get_bv_sid(to_width);
 356                                 int nid2 = next_nid++;
 357                                 btorf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1);
 358                                 nid = nid2;
 359                         }
 360                         else
 361                         {
 362                                 int sid = get_bv_sid(to_width);
 363                                 int nid2 = next_nid++;
 364                                 btorf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext",
 365                                                 sid, nid, to_width - GetSize(sig));
 366                                 nid = nid2;
 367                         }
 368                 }
 369
 370                 return nid;
 371         }
 372
 373         BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
 374                         f(f), sigmap(module), module(module), verbose(verbose)
 375         {
 376                 btorf_push("inputs");
 377
 378                 for (auto wire : module->wires())
 379                 {
 380                         if (!wire->port_id || !wire->port_input)
 381                                 continue;
 382
 383                         SigSpec sig = sigmap(wire);
 384                         int sid = get_bv_sid(GetSize(sig));
 385                         int nid = next_nid++;
 386
 387                         btorf("%d input %d %s\n", nid, sid, log_id(wire));
 388                         add_nid_sig(nid, sig);
 389                 }
 390
 391                 btorf_pop("inputs");
 392
 393                 for (auto cell : module->cells())
 394                 for (auto &conn : cell->connections())
 395                 {
 396                         if (!cell->output(conn.first))
 397                                 continue;
 398
 399                         for (auto bit : sigmap(conn.second))
 400                                 bit_cell[bit] = cell;
 401                 }
 402
 403                 for (auto wire : module->wires())
 404                         if (wire->port_output)
 405                                 output_symbols.insert(log_id(wire));
 406
 407                 for (auto wire : module->wires())
 408                 {
 409                         if (!wire->port_id || !wire->port_output)
 410                                 continue;
 411
 412                         btorf_push(stringf("output %s", log_id(wire)));
 413
 414                         int sid = get_bv_sid(GetSize(wire));
 415                         int nid = get_sig_nid(wire);
 416                         btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
 417
 418                         btorf_pop(stringf("output %s", log_id(wire)));
 419                 }
 420
 421                 for (auto cell : module->cells())
 422                 {
 423                         if (cell->type == "$assume")
 424                         {
 425                                 btorf_push(log_id(cell));
 426
 427                                 int sid = get_bv_sid(1);
 428                                 int nid_a = get_sig_nid(cell->getPort("\\A"));
 429                                 int nid_en = get_sig_nid(cell->getPort("\\EN"));
 430                                 int nid_not_en = next_nid++;
 431                                 int nid_a_or_not_en = next_nid++;
 432                                 int nid = next_nid++;
 433
 434                                 btorf("%d not %d %d\n", nid_not_en, sid, nid_en);
 435                                 btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en);
 436                                 btorf("%d constraint %d\n", nid, nid_a_or_not_en);
 437
 438                                 btorf_pop(log_id(cell));
 439                         }
 440
 441                         if (cell->type == "$assert")
 442                         {
 443                                 btorf_push(log_id(cell));
 444
 445                                 int sid = get_bv_sid(1);
 446                                 int nid_a = get_sig_nid(cell->getPort("\\A"));
 447                                 int nid_en = get_sig_nid(cell->getPort("\\EN"));
 448                                 int nid_not_a = next_nid++;
 449                                 int nid_en_and_not_a = next_nid++;
 450                                 int nid = next_nid++;
 451
 452                                 btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
 453                                 btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
 454                                 btorf("%d bad %d\n", nid, nid_en_and_not_a);
 455
 456                                 btorf_pop(log_id(cell));
 457                         }
 458                 }
 459
 460                 while (!ff_todo.empty())
 461                 {
 462                         vector<pair<int, Cell*>> todo;
 463                         todo.swap(ff_todo);
 464
 465                         for (auto &it : todo)
 466                         {
 467                                 btorf_push(stringf("next %s", log_id(it.second)));
 468
 469                                 SigSpec sig = sigmap(it.second->getPort("\\D"));
 470
 471                                 int nid = get_sig_nid(sig);
 472                                 int sid = get_bv_sid(GetSize(sig));
 473                                 btorf("%d next %d %d %d\n", next_nid++, sid, it.first, nid);
 474
 475                                 btorf_pop(stringf("next %s", log_id(it.second)));
 476                         }
 477                 }
 478         }
 479 };
 480
 481 struct BtorBackend : public Backend {
 482         BtorBackend() : Backend("btor", "write design to BTOR file") { }
 483         virtual void help()
 484         {
 485                 //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 486                 log("\n");
 487                 log("    write_btor [options] [filename]\n");
 488                 log("\n");
 489                 log("Write a BTOR description of the current design.\n");
 490                 log("\n");
 491                 log("  -v\n");
 492                 log("    Add comments and indentation to BTOR output file\n");
 493                 log("\n");
 494         }
 495         virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 496         {
 497                 bool verbose = false;
 498
 499                 log_header(design, "Executing BTOR backend.\n");
 500
 501                 size_t argidx;
 502                 for (argidx = 1; argidx < args.size(); argidx++)
 503                 {
 504                         if (args[argidx] == "-v") {
 505                                 verbose = true;
 506                                 continue;
 507                         }
 508                         break;
 509                 }
 510                 extra_args(f, filename, args, argidx);
 511
 512                 RTLIL::Module *topmod = design->top_module();
 513
 514                 if (topmod == nullptr)
 515                         log_cmd_error("No top module found.\n");
 516
 517                 *f << stringf("; BTOR description generated by %s for module %s.\n",
 518                                 yosys_version_str, log_id(topmod));
 519
 520                 BtorWorker(*f, topmod, verbose);
 521
 522                 *f << stringf("; end of yosys output\n");
 523         }
 524 } BtorBackend;
 525
 526 PRIVATE_NAMESPACE_END